Proving A ≤ B or B ≤ A from Trichotomy.

[solakis1]

given the definition: $$A\leq B\Longleftrightarrow A<B\vee A=B$$ Where A,B are reals ,then prove:

$$A\leq B\vee B\leq A$$

Proof: From trichotomy we have : (a<bva=b)vb<a=> [(a<bva=b)vb<a]vb=a =>(a<bva=b)v(b<avb=a).

And here is where i get stuck.

According to which law in propusitional calculus can we substitute (a<bva=b) and (b<avb=a) with $$A\leq B$$ and [math] B\leq A[/math] according to the above definition??

 

[Fallen Angel]

Hi,

It's just the definition at the beginning of your post.

 

[Evgeny.Makarov]

Replacing $A<B\lor A=B$ with $A\le B$ is not a question of object calculus, but of metacalculus (our natural language). For example, if you decide to write $f$ instead of $5$, you don't need a new arithmetic identity to conclude that $f+1=6$. The arithmetic "does not see", so to speak, your abbreviation. From its standpoint the equation is $5+1=6$. It's only your way of writing this equation that changed.

Similarly, if $B\le A$ is defined as $B<A\lor B=A$, then this is simply an abbreviation that makes out writing shorter. This definition is transparent on the object level, and the formulas you derive still contain $B<A\lor B=A$.

Another option is to treat $\le$ as a primitive predicate symbol and not a definition. Then one must posit an axiom
\[
B\le A\leftrightarrow B<A\lor B=A.
\]
Suppose a formula $F$ that contains a subformula $B<A\lor B=A$ is derivable. Then $F'$, which is obtained from $F$ by replacing $B<A\lor B=A$ with $B\le A$ is also derivable. This is a metatheorem that is proved by induction on $F$.

 

[solakis1]

Replacing $A<B\lor A=B$ with $A\le B$ is not a question of object calculus, but of metacalculus (our natural language). For example, if you decide to write $f$ instead of $5$, you don't need a new arithmetic identity to conclude that $f+1=6$. The arithmetic "does not see", so to speak, your abbreviation. From its standpoint the equation is $5+1=6$. It's only your way of writing this equation that changed.

Similarly, if $B\le A$ is defined as $B<A\lor B=A$, then this is simply an abbreviation that makes out writing shorter. This definition is transparent on the object level, and the formulas you derive still contain $B<A\lor B=A$.

Another option is to treat $\le$ as a primitive predicate symbol and not a definition. Then one must posit an axiom
\[
B\le A\leftrightarrow B<A\lor B=A.
\]
Suppose a formula $F$ that contains a subformula $B<A\lor B=A$ is derivable. Then $F'$, which is obtained from $F$ by replacing $B<A\lor B=A$ with $B\le A$ is also derivable. This is a metatheorem that is proved by induction on $F$.

Thank you, I always get mixed up with theorems and metatheorems.
But do you mean that except the rule of equivalence substitution ,no other rules of propositional calculus can be used to solve the problem??

 

[Evgeny.Makarov]

But do you mean that except the rule of equivalence substitution ,no other rules of propositional calculus can be used to solve the problem?

If $\le$ is a primitive predicate symbol and inequality is defined by an axiom, then you do need the rule of equivalence substitution. However, this rule is a metatheorem and uses various inference rules of the underlying calculus to build a new derivation. Which rules exactly are used depends on the calculus.

 

[solakis1]

. Which rules exactly are used depends on the calculus.

Suppose we are given the following rules:

Double negation
conjunctio introduction
conjunction elimination
disjunction introduction
disjunction elimination
conditional proof
contradiction
bicondtional introduction
biconditional elimination.

How would we solve the problem