A Prover for the Propositional Fragment of First-Order Logic

Mircea Marin

We consider the fragment of propositional logic where propositions built with the logical connectives: ∧ (conjunction), ∨ (disjunction), ⟹ (implication) and ¬ (negation), and employ Gentzen's system G' for deciding whether a formula.(Subscript[Q, 1]) ∨… ∨ (Subscript[Q, q]) follows from the formula (Subscript[P, 1])∧…∧ (Subscript[P, p]). It is well-known that ((Subscript[P, 1])∧…∧ (Subscript[P, p])) => ((Subscript[Q, 1]) ∨… ∨ (Subscript[Q, q])) holds iff the sequent

{(Subscript[P, 1]),…, (Subscript[P, p])}⊢{(Subscript[Q, 1]),…, (Subscript[Q, q])}

can be inferred from the system G' of inference rules shown below:

({{ {(Subscript[Γ, 1]),A,(Subscript[Δ, 1])}⊢{(Subscript[Γ, 2]),A,(Subscript[Δ, 2])},  }, {(({Γ,A,B,Δ}⊢R)/({Γ,A∧B,Δ}⊢R)), ((L⊢{Δ,A,Λ}   L⊢{Δ,B,Λ} )/(L⊢{Δ,A∧B,Λ} ))}, {(({Δ,A,Λ}⊢R   {Δ,B,Λ}⊢R)/({Δ,A∨B,Λ}⊢R)), ((L⊢{Γ,A,B,Δ})/(L⊢{Γ,A∨B,Δ}))}, {(({Γ,Δ}⊢{A,Λ}  {B,Γ,Δ}⊢{Λ})/({Γ,A⟹B,Δ}⊢{Λ})), (({A,Γ}⊢{B,Δ,Λ})/({Γ}⊢{Δ,A⟹B,Λ}))}, {(({Γ,Δ}⊢{A,Λ})/({Γ,¬A,Δ}⊢{Λ})), (({A,Γ}⊢{Δ,Λ})/({Γ}⊢{Δ,¬A,Λ}))}})

(* Evaluate this, to instruct Mathematica to to ignore the built-in interpretation of ¬ *)
MakeExpression[RowBox[{"¬",t_}],form_]:=MakeExpression[RowBox[{"No","[",t,"]"}],form];
No/:MakeBoxes[No[t_],form_]:=RowBox[{"¬",MakeBoxes[t,form]}];

The system G' has a straightforward implementation in ρLog:

<<RhoLog`;
DeclareRules[
"Axiom"∷({((_)^s),(A^i),((_)^s)}⊢{((_)^s),(A^i),((_)^s)}),
"⋀-Left"∷({(Γ^s),(A^i)⋀(B^i),(Δ^s)}⊢(R^i))⟸("G'"∷({(Γ^s),(A^i),(B^i),(Δ^s)}⊢(R^i))),
"⋀-Right"∷((L^i)⊢{(Δ^s),(A^i)⋀(B^i),(Λ^s)})⟸("G'"∷((L^i)⊢{(Δ^s),(A^i),(Λ^s)})&&"G'"∷((L^i)⊢{(Δ^s),(B^i),(Λ^s)})),
"⋁-Left"∷({(Δ^s),(A^i)⋁(B^i),(Λ^s)}⊢(R^i))⟸("G'"∷({(Δ^s),(A^i),(Λ^s)}⊢(R^i))&&"G'"∷({(Δ^s),(B^i),(Λ^s)}⊢(R^i))),
"⋁-Right"∷((L^i)⊢{(Γ^s),(A^i)⋁(B^i),(Δ^s)})⟸("G'"∷((L^i)⊢{(Γ^s),(A^i),(B^i),(Δ^s)})),
"⟹-Left"∷({(Γ^s),(A^i)⟹(B^i),(Δ^s)}⊢{(Λ^s)})⟸("G'"∷({(Γ^s),(Δ^s)}⊢{(A^i),(Λ^s)})&&"G'"∷({(B^i),(Γ^s),(Δ^s)}⊢{(Λ^s)})),
"⟹-Right"∷({(Γ^s)}⊢{(Δ^s),(A^i)⟹(B^i),(Λ^s)})⟸("G'"∷({(A^i),(Γ^s)}⊢{(B^i),(Δ^s),(Λ^s)})),
"¬-Left"∷({(Γ^s),¬(A^i),(Δ^s)}⊢{(Λ^s)})⟸("G'"∷({(Γ^s),(Δ^s)}⊢{(A^i),(Λ^s)})),
"¬-Right"∷({(Γ^s)}⊢{(Δ^s),¬(A^i),(Λ^s)})⟸("G'"∷({(A^i),(Γ^s)}⊢{(Δ^s),(Λ^s)})),
"G'"∷(F^i)⟸("Or"["Axiom","¬-Left","¬-Right","⋀-Left","⋁-Right","⟹-Right","⋀-Right","⋁-Left","⟹-Left"]∷(F^i))
]

Note that we preferred to give distinctive names to the inference rules of G'.

Tests

Let's check whether the formula (P⟹Q)⟹((¬Q)⟹(¬P)) is a tautology or not. This amounts to checking whether the relation

"G'"∷({}⊢{(P⟹Q)⟹((¬Q)⟹(¬P))})

holds w.r.t. our rule definitions.

Request["G'"∷({}⊢{(P⟹Q)⟹((¬Q)⟹¬P)}),Trace->True]

The following call indicates that the formula P⟹Q is not a tautology.

Request["G'"∷({}⊢{P⟹Q}),Trace->True]

whereas the call

Request["G'"∷({}⊢{(A⋁B)⋁((¬A)⋀¬B)}),Trace->True]

indicates that the formula (A⋁B)∨(¬A∧¬B) is a tautology.

Request[{}⊢{(P⟹Q)⟹((¬Q)⟹(¬P))}(Subscript[->, "G'"])True,Trace->True]