Skip to content

HSC_AX

Jump to bottom Edit New page
Andrej Dudenhefner edited this page Nov 21, 2019 · 1 revision

Recognizing axiomatizations of Hilbert-style calculi

This problem was posed by Tarski in 1946 and first studied by Linial and Post [1]. Recent results include a strengthened formulation by Bokov [2] and Dudenhefner [3].

Preliminaries

The definitions below are mechanized in Problems/HSC.v.

Formulas s, t are defined as s, t ∈ 𝔽 ::= a | s β†’ t, where a ∈ 𝔸 ranges over atoms. Formulas are mechanized as formula, where 𝔸 is mechanized as nat.

A substitution ΞΆ : 𝔸 β†’ 𝔽 is lifted to formulas by ΞΆ (s β†’ t) = ΞΆ (s) β†’ ΞΆ (t).

An environment Ξ“ is a list of formulas.

A formula t is derivable from Ξ“ in a Hilbert-style calculus, if

  • there is a formula s in Ξ“ and substitution ΞΆ such that t = ΞΆ (s), or
  • there is a formula s such that both formulae s and s β†’ t are derivable from Ξ“.

The above is mechanized as the inductive predicate hsc (Gamma: list formula) : formula -> Prop.

Problem instance (mechanized as HSC_AX_PROBLEM)

An instance of recognizing axiomatizations of Hilbert-style calculi is a list [s₁, …,sβ‚™] of formulas such that sα΅’ is derivable from [a β†’ (b β†’ a)] for i = 1 … n.

Decision problem (mechanized as HSC_AX)

Given a problem instance Ξ“, is the formula a β†’ (b β†’ a) derivable from Ξ“?

Reduction

Undecidability of recognizing axiomatizations of in Hilbert-style calculi is obtained by reduction from binary modified Post correspondence problem (BMPCP in Problems/PCP.v). The reduction is mechanized in Reductions/BMPCP_to_HSC.v as

Theorem BMPCP_to_HSC_AX : BMPCP βͺ― HSC_AX.

and

Theorem HSC_AX_undec : Halt βͺ― HSC_AX.

Key ideas [3]

Let formula constructor β†’ associate to the right.

Fix an atom β€’ ∈ 𝔸.

The binary symbols 0 and 1 are encoded by formulas '0 := β€’ β†’ β€’ and '1 := β€’ β†’ β€’ β†’ β€’ respectively.

Concatenation of a formula s with a binary word v = x₁ … xβ‚™ is encoded by the formula s + v := 'xβ‚™ β†’ … β†’ 'x₁ β†’ s.

A pair (s, t) of formulas is encoded by the formula '(s, t) := (β€’ β†’ β€’ β†’ β€’) β†’ s β†’ t β†’ β€’ β†’ β€’ β†’ β€’.

An instance of binary modified Post correspondence problem is a pair (v, w) of binary words and a list P of pairs of binary words; it is represented by the environment

Ξ“ = ['(a, a), '(β€’ + v, β€’ + w) β†’ β€’ β†’ a β†’ β€’] ++ (map (fun (x, y) => '(a + x, b + y) β†’ '(a, b)) P)

If the formula a β†’ b β†’ a is derivable from Ξ“, then so is the formula '(β€’ + v, β€’ + w).

The formulae '(a + x, b + y) β†’ '(a, b) in Ξ“ where (x, y) ∈ P necessitate derivability of ever longer pairs of words consistent with reachability in the given Post correspondence problem instance. Ultimately, the formula '(a, a) finishes the derivation equating the first with the second element of the encoded binary word pair.

The main instrument to restrict the shape of derivations is the formula β€’ β†’ β€’ β†’ β€’ appearing as the first argument of '(s, t). If there is a derivation of an instance of β€’ β†’ β€’ β†’ β€’, then there is a minimal derivation of an instance of '(β€’ + v, β€’ + w) with no nested derivation of a (possibly different) instance of β€’ β†’ β€’ β†’ β€’. Therefore, such a minimal derivation, for example, can use the formula '(a, a) only at leaf positions.

Mechanization remarks

The previous mechanization [3] (1700 lines of code) uses the Lean proof assistant and relies on classical reasoning. In particular, minimal derivations are introduced via excluded middle. The present mechanization (600 lines of code) uses a constructive, mutually inductive argument that combines proof minimization with proof reconstruction.

Related problems

Surprisingly, the construction fails when a β†’ (b β†’ a) replaced by a β†’ (b β†’ b) because recognizing axiomatizations of a β†’ (b β†’ b) is decidable in polynomial time [3].

A fortiori, provability in Hilbert-style calculi, i. e. given an environment Ξ“ and a formula s, is s derivable from Ξ“?, is undecidable. Notably, Theorem HSC_AX_undec is restricted to a family of sub-intuitionistic environments and the fixed formula a β†’ (b β†’ a).

Complementarily, there exists an environment Ξ“ for which provability is undecidable (HSC_PRV).

References

[1] Samuel Linial and Emil L. Post: Recursive unsolvability of the deducibility, Tarski’s completeness and independence of axioms problems of propositional palculus. Bulletin of the American Mathematical Society, 55:50, 1949.

[2] Grigoriy V. Bokov: Undecidable problems for propositional calculi with implication. Logic Journal of the IGPL, 24(5):792–806, 2016. doi:10.1093/jigpal/jzw013

[3] Andrej Dudenhefner, Jakob Rehof: Lower end of the Linial-Post spectrum. TYPES 2017: 2:1-2:15. doi: 10.4230/LIPIcs.TYPES.2017.2

Add a custom footer
Add a custom sidebar
Clone this wiki locally