"Every proposition of logic is a modus ponens represented in signs" (Wittgenstein, Tractatus 6.1264).
"Since it is possible to get by with only one means of inference [modus ponens], then it is a precept of clarity to do so" (Frege).
"Logic has no existence independent of mathematics" (Tobias Dantzig).
Direct Condition
Semantics
Whether or not to consider a certain expression x depending on whether another expression y exists:
If the expression y exists (i.e., if y≠θ), then the result is x.
If the expression y does not exist (i.e., if y=θ), then the result of the operation is the null expression (θ).
The expression y is called "condition". The expression x is the "action" to be taken if the condition is met.
Syntax
(x ← y) // x if y
or
(y → x) // if y, then x
The mnemonic rule is that the symbol points to the action.
Justification
The condition is the basic element of the decision, which allows us to consider something or not based on a specific circumstance (the condition).
Examples
(a = 3)
((x + y) ← a) // ev. (x + y)
(x = 1)
(y = 2)
(a ← (x+y)) // ev. a
(b = θ)
((a b c) ← b) // ev. θ
(x = 1)
(y = 2)
((z = x+y) ← α) // ev. (z = 3)
(a = 2)
(b = 3)
(x ← a=b) // ev. θ
(x ← (a =' b)) // ev. x
(x ← (a ≠ b)) // ev. x
(x ← a>b) // ev. θ
(x ← a≥b) // ev. θ
(x ← a<b) // ev. x
(x ← a≤b) // ev. x
(a = 2)
(b = 2)
(x ← a≡b) // ev. x
(x ← (a ≡' b)) // ev. θ
x←{a b} // ev. {a b}
Remarks
Logical values (true or false) are not used as conditions. Instead, the concept of existence is used, represented by the metaexpressions α (existence) and θ (non-existence).
For obvious reasons of computational economy, in a conditional expression the condition is evaluated first, regardless of the physical order of the condition and action expressions.
In a conditional expression there is symmetry on both sides of the operator (the two expressions can be of either type). This is not the case with the condition of traditional programming languages, which must necessarily be a logical expression that evaluates to true or false.
A condition can also be an arithmetic comparison, substitution or equivalence expression, as well as their opposites, as shown in the examples. In the case of substitution, we are asking whether or not such a substitution is fulfilled, so such a substitution is not made. The same is true for the subject of equivalence.
Logical implication is implemented by a generic expression. For example:
⟨( x=b ←' n>3 → x=a )⟩
n=7 // automatically implies x=a
x // ev. a
n=1 // automatically implies x=b
x // ev. b
Axioms
⟨( (x ← y) ≡ (y → x) )⟩ //by definition
⟨( (x ← θ) = θ )⟩ // by definition
⟨( (x ← α) = x )⟩
The expression α acting as a condition is a universal condition, and is the default condition of every expression (i.e., if no condition is specified).
⟨( (x ← ()) = x )⟩ // the empty sequence exists
⟨( (x ← (y = y)) = x )⟩
⟨( (x ← (y =' y)) = θ )⟩
⟨( (x ← (y ≡ y)) = x )⟩
⟨( (x ← (y ≡' y)) = θ )⟩
⟨( (x ← x) = x )⟩ // idempotence
In effect:
If x≠θ, (x←x) ev. x
If x=θ, (x←x) ev. θ
