HSC_PRV

Provability in a fixed Hilbert-style calculus

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_PRV_PROBLEM)

Fix an environment Γ. An instance of provability in a Hilbert-style calculus is a formula s.

Decision problem (mechanized as HSC_PRV)

Given a formula s, is s derivable from the fixed environment Γ?

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_PRV : BMPCP ⪯ HSC_PRV ΓPCP.

and

Theorem HSC_PRV_undec : Halt ⪯ HSC_PRV ΓPCP.

where ΓPCP is a fixed environment.

Key ideas

Similarly to HSC_AX, we encode binary symbols and pairs using a fixed atom •.

The empty list is encoded by • and the list a :: A is encoded by the encoding of the pair ('a, 'A), where 'a and 'A encode a and A respectively.

A state is the pair ((Q, P), (x, y)) where P is the list of word pairs given by the binary modified Post correspondence problem instance, Q is a suffix of P, and x, y are constructed by respective repeated concatenation of words from P.

The fixed environment ΓPCP consists of encodings of the following state transitions

((Q, P), (x, x)) (* termination, equality *)
((P, P), (x ++ v), (y ++ w))) → ((((v, w) :: Q), P), (x, y)) (* concatenation *)
((Q, P), (x, y)) → ((((v, w) :: Q), P), (x, y))  (* search *)
((Q, P), ((x ++ [a]) ++ v), y)) → ((Q, P), ((x ++ (a :: v)), y)) (* associativity *)
((Q, P), (x, (y ++ [a]) ++ w))) → ((Q, P), (x, (y ++ (a :: w)))) (* associativity *)

Overall, a binary modified Post correspondence problem instance ((v, w), P) is solvable iff the formula encoding the state ((((v, w) :: P), ((v, w) :: P)), (v, w)) is provable from ΓPCP.

The main instrument to restrict the shape of derivations is the formula • → • → •, appearing as the first argument of pair encoding. In particular, no instance of • → • → • is derivable in ΓPCP, heavily restricting the shape of derivations. For example, the formula encoding ((Q, P), (x, x)) can be used only at leaf positions.

References

[1] Wilson E. Singletary: Many-one Degrees Associated with Partial Propositional Calculi. Notre Dame Journal of Formal Logic, XV(2):335–343, 1974.

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