Formal Methods 101: Formal Systems

Introduction:

• A Formal System is a set of formulas (axioms, or derived from axioms) that are used to infer properties, theorems, or additional truths.

• Axioms can be thought of as a set of given assumptions or rules about a formal system.

• An interpretation of the axioms (and truths derived from the axioms) is known as a model. For example, in first-order logic without quantifiers and only Boolean valued variables, a model would be one assignment of Boolean values to the predicate variables. All possible models would be all possible assignments of Boolean values to the predicate variables. For FOL expressions without quantifies and only Boolean valued variables (i.e. basic predicates), all possible models can be expressed by a truth table.
  • Ex. FOL Expression (Basic Predicate): P = (A ∧¬B) | A,B ∈ {0,1}

• In order to discuss this topic we need to introduce some new symbols:

• Syntactic Entailment: ⊢
  • Also known as syntactic consequence, syntactic implication, syntactic consequence, or logical implication. Functionally the same as the binary version known as material implication, but is in the ‘meta’ context of a system.
  • Given Γ, which is the set of formulas (axioms, or derived from axioms) of Formal System S, and Property ϕ, we write Γ⊢ϕ
    • This says that property ϕ is provable (derivable) from the set of formulas (axioms or rules) Γ given by the Formal System S. (Sometimes written Γ⊦_S ϕ).

• Semantic Entailment: ⊨
  • Also known as syntactic consequence, semantic implication, or semantic consequence. This relates to truths that are true within the) of set of formulas (axioms, or derived from axioms) Γ given by the Formal System S.
  • Given Γ, which is the set of formulas (axioms, or derived from axioms) of Formal System S, and Property ϕ, we write Γ ⊨ ϕ
    • This says that property ϕ is true (not necessarily derivable) in all models (all possible interpretations) of a set of formulas (axioms, or derived from axioms) Γ of a Formal System S. (Sometimes written Γ ⊦_S ϕ)

• Intuition on the differences between syntactic entailment and semantic entailment.

• Syntactic Entailment:
  • Given Axioms Γ = {((A ∧¬B) → C), ((C ∨D) → E)}, does ϕ = ((A ∧¬B ∨ D) →  E) hold?
  • Derivation:
    • 1. (A ∧¬B) → C
    • 2. (C ∨D) → E
    • 3. Substitute 1 into 2 and get (A ∧¬B ∨ D) → E)

• Because ϕ is syntactically derivable from Γ, we can write  Γ⊢ϕ.

• Semantic Entailment:
  • Given Axioms Γ = {((A ∧¬B) → C), ((C ∨ D) → E)}
  • Does ϕ = ((A ∧¬B ∨ D) →  E) hold?
    • If we look at the models (assignments that make the predicates true), we can see that there are no models (possible interpretations) of ϕ for which the models of axioms Γ(0), Γ(1) are contradictory to the implication of E.

• Because ϕ is semantically valid from Γ, we can write Γ ⊨ ϕ.

• Semantic Completeness
  • A formal system is semantically complete if every all tautologies are theorems (derivable truths).
  • ( ⊨ ϕ) → ( ⊦ ϕ).
• Strong Completeness
  • A formal system is Strongly Complete if every semantic truth in the system can be syntactically derived (proved). (i.e. every truth is provable)
    (Γ ⊨ ϕ) → (Γ⊦ ϕ).
    Intuitively, strongly complete means that given Γ, it is possible to compute all semantic consequences.
• Refutation-Complete
  • A formal system S is Refutation-Complete if it is able to derive false from every set of formulas that are unsatisfiable.
    (Γ ⊨ ⊥) → (Γ⊦ ⊥)
  • All Strongly Complete systems are also Refutation-Compete. Intuitively, refutation-complete means that it is possible to check if ϕ is a semantic consequence.
• Soundness
  • A formal system is Sound if every derivable (provable) syntactic truth in the system is a semantic truth. (i.e. no FALSE truth can be proved)
  • (Γ⊦ ϕ)→(Γ ⊨ ϕ)

Zero-Order (Propositional) Logic is both Sound and Complete.