# Use Hilbert style proofs to solve problem

Solve this problem by using Hilbert style proof:

$A,B \vdash A \equiv B$

my try :

• (1) A (hyp)
• (2) B (hyp)
• (3) $A \land B$ (merge)
• (4) $A \land B \equiv A \equiv B \equiv A \lor B$ (golden rule)
• (5) $A \equiv B \equiv A \lor B$ (3,4 + equ)
• (6) $A \lor B \equiv A \equiv B$ (Symmetry)

That was my try. I don't know if it was right. I couldn't continue.

Inference rules : leibniz and equanimity.

Lists of axioms and theorems :

• What are the axioms and/or rules of inference of your system? – Doug Spoonwood Feb 3 '14 at 4:51
• @DougSpoonwood Please see my edit for the axioms and rules of inference. – Out Of Bounds Feb 3 '14 at 5:04

We will start from George Tourlakis, Mathematical Logic (2008), Example 2.5.1(1), page 77 :

(1) $\quad A, B \vdash A \land B$

and use the Golden Rule, page 43 :

$$(A \land B) \equiv (A \equiv (B \equiv A \lor B))$$

Applying Equanimity [page 40], from (1) we have :

(2) $\quad A,B \vdash (A \equiv (B \equiv A \lor B))$

From the axiom about Associativity of $\equiv$ : $(A \equiv (B \equiv C)) \equiv (A \equiv B) \equiv C)$, by Equanimity :

(3) $\quad A,B \vdash (A \equiv B) \equiv (A \lor B)$

Using again Example 2.5.1(3) :

(4) $\quad A \vdash A \lor B$

we apply again Equanimity :

(5) $\quad A,B \vdash (A \equiv B)$.