Understanding Propositional Logic Laws

1.Logical Equivalence:

2.Consistency & Inconsistency:

3.Implication (Entailment / Logical Consequence):

4. Independence:

5.Validity & Invalidity:

6.Satisfiability & Unsatisfiability:

Hilbert Proof System in Propositional Logic




A. Axioms (3 Schemas)




A1: A → (B → A)

Self-evidence axiom: Any proposition implies that any other proposition implies the first one. This captures the idea that if something is true, it remains true regardless of what other assumptions you make.



A2: (A → (B → C)) → ((A → B) → (A → C))

Distribution axiom: If A implies that B implies C, and A also implies B, then A must imply C directly. This enables chain reasoning and logical distribution.



A3: (¬B → ¬A) → (A → B)

Contrapositive axiom: If the negation of B implies the negation of A, then A implies B. It gives one direction of the equivalence between a statement and its contrapositive; the other direction, from "A implies B" to "not B implies not A", is provable from the axioms.


Pitfall: Taking the inverse for the contrapositive
Writing $\neg A \to \neg B$ as the contrapositive of $A \to B$ fails at the row $A = F$, $B = T$: there $A \to B$ is T but $\neg A \to \neg B$ is F. The contrapositive is $\neg B \to \neg A$, which matches $A \to B$ in every row.
Read more
In A3 the two letters change places as they gain their negations: $B$, the consequent of the conclusion $A \to B$, stands negated before the arrow in the hypothesis, and $A$ stands negated after it. With $A$ = "it rains" and $B$ = "the ground is wet", the hypothesis reads "if the ground is not wet, then it does not rain", and the conclusion reads "if it rains, the ground is wet".



B. Premises




Definition

Premises are the starting assumptions in a proof. They serve as the foundation from which conclusions are derived.



Types:

1. Logical premises: The axiom schemas above, universally valid
2. Domain premises: Specific assumptions given for a particular proof
3. Temporary premises: Assumptions made for conditional or indirect proofs



Role in proofs:

Premises establish the initial truth conditions. All subsequent steps must follow logically from these starting points using valid inference rules.



C. Inference Rules




Modus Ponens (MP)

Rule: From A and A → B, derive B
Purpose: The only inference rule needed in pure Hilbert systems. It allows you to detach the consequent of an implication when you have both the implication and its antecedent.



Substitution (Implicit)

Rule: Replace variables in axiom schemas with any well-formed formulas
Purpose: Generates specific instances of the general axiom patterns for use in particular proofs.



Proof Construction

Pitfall: Affirming the consequent
Deriving $A$ from $A \to B$ and $B$ is not modus ponens: at the row $A = F$, $B = T$ both premises are T while $A$ is F. Modus ponens needs the antecedent $A$, and then gives $B$.
Read more
A proof is a finite sequence of formulas where each formula is either:

• A premise (axiom or assumption)
• Derived from previous formulas by Modus Ponens

The system is complete (proves all tautologies) and sound (proves only tautologies).

Even a formula as plain as $A \to A$ is not an axiom here, so it has to be derived. Every line of the derivation must be an instance of A1, A2 or A3, or follow from two earlier lines by modus ponens; nothing else may be written down, however obvious it looks.


Fact: Five lines to prove $A \to A$
The usual derivation of $A \to A$ in this system takes five lines: one instance of A2, with $A \to A$ in place of $B$ and $A$ in place of $C$, two instances of A1, and modus ponens twice. With three axioms and one rule, even the most obvious tautology is built step by step.

A proof in this system may be long, but checking it is mechanical. Each line is compared with the three axiom patterns, or with two earlier lines and the shape of modus ponens. No idea of what the formulas mean is needed for the check, which is why such proofs can be verified by a computer.


Three axiom patterns and one rule are enough to prove every tautology, and nothing but tautologies.