I'm trying to prove the statement ~(a->~b) => a in a Hilbert style system. Unfortunately it seems like it is impossible to come up with a general algorithm to find a proof, but I'm looking for a brute force type strategy. Any ideas on how to attack this are welcome.

# R – Hilbert System – Automate Proof

computer-sciencelogicmaththeorem-provingverification

## Best Solution

If You like "programming" in combinatory logic, then

The possibility of this translation in ensured by Curry-Howard correspondence.

Unfortunately, the situation is so simple only for a subset of (propositional) logic: restricted using conditionals. Negation is a complication, I know nothing about that. Thus I cannot answer this concrete question:

¬ (

α⊃ ¬β) ⊢αBut in cases where negation is not part of the question, the mentioned automatic translation (and back-translation) can be a help, provided that You have already practice in functional programming or combinatory logic.

Of course, there are other helps, too, where we can remain inside the realm of logic:

As for theorem provers, as far as I know, the capabilities of some of them are extended so that they can harness interactive human assistance. E.g. Coq is such.

## Appendix

Let us see an example. How to prove

α⊃α?## Hilbert system

Verum ex quolibet_{α,β}is assumed as an axiom scheme, stating that sentenceα⊃β⊃αis expected to be deducible, instantiated for any subsentencesα,βChain rule_{α,β,γ}is assumed as an axiom scheme, stating that sentence (α⊃β⊃γ) ⊃ (α⊃β) ⊃α⊃γis expected to be deducible, instantiated for any subsentencesα,βModus ponensis assumed as a rule of inference: provided thatα⊃βis deducible, and alsoαis deducible, then we expect to be justified to infer that alsoα⊃βis deducible.Let us prove theorem:

α⊃αis deducible for anyαproposition.Let us introduce the following notations and abbreviations, developing a "proof calculus":

## Proof calculus

VEQ_{α,β}: ⊢α⊃β⊃αCR_{α,β,γ}: ⊢ (α⊃β⊃γ) ⊃ (α⊃β) ⊃α⊃γMP: If ⊢α⊃βand ⊢α, then also ⊢βA tree diagram notation:

## Axiom scheme — Verum ex quolibet:

━━━━━━━━━━━━━━━━━ [

VEQ_{α,β}]⊢

α⊃β⊃α## Axiom scheme — chain rule:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [

CR_{α,β,γ}]⊢ (

α⊃β⊃γ) ⊃ (α⊃β) ⊃α⊃γ## Rule of inference — modus ponens:

⊢

α⊃β⊢α━━━━━━━━━━━━━━━━━━━ [

MP]⊢

β## Proof tree

Let us see a tree diagram representation of the proof:

━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [

CR_{α, α⊃α, α}] ━━━━━━━━━━━━━━━ [VEQ_{α, α⊃α}]⊢ [

α⊃(α⊃α)⊃α]⊃(α⊃α⊃α)⊃α⊃α⊢α⊃ (α⊃α) ⊃α━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [

MP] ━━━━━━━━━━━ [VEQ_{α,α}]⊢ (

α⊃α⊃α) ⊃α⊃α⊢α⊃α⊃α━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ [

MP]⊢

α⊃α## Proof formulae

Let us see an even conciser (algebraic? calculus?) representation of the proof:

(

CR_{α,α⊃α,α}VEQ_{α,α ⊃ α})VEQ_{α,α}: ⊢α⊃αso, we can represent the proof tree by a single formula:

It is worth of keep record about the concrete instantiation, that' is typeset here with subindexical parameters.

As it will be seen from the series of examples below, we can develop a

proof calculus, where axioms are notated as sort ofbase combinators, and modus ponens is notated as a mereapplicationof its "premise" subproofs:## Example 1

VEQ_{α,β}: ⊢α⊃β⊃αmeant as

Verum ex quolibetaxiom scheme instantiated withα,βprovides a proof for the statement, thatα⊃β⊃αis deducible.## Example 2

VEQ_{α,α}: ⊢α⊃α⊃αVerum ex quolibetaxiom scheme instantiated withα,αprovides a proof for the statement, thatα⊃α⊃αis deducible.## Example 3

VEQ_{α, α⊃α}: ⊢α⊃ (α⊃α) ⊃αmeant as

Verum ex quolibetaxiom scheme instantiated withα,α⊃αprovides a proof for the statement, thatα⊃ (α⊃α) ⊃αis deducible.## Example 4

CR_{α,β,γ}: ⊢ (α⊃β⊃γ) ⊃ (α⊃β) ⊃α⊃γmeant as

Chain ruleaxiom scheme instantiated withα,β,γprovides a proof for the statement, that (α⊃β⊃γ) ⊃ (α⊃β) ⊃α⊃γis deducible.## Example 5

CR_{α,α⊃α,α}: ⊢ [α⊃ (α⊃α) ⊃α] ⊃ (α⊃α⊃α) ⊃α⊃αmeant as

Chain ruleaxiom scheme instantiated withα,α⊃α,αprovides a proof for the statement, that [α⊃ (α⊃α) ⊃α] ⊃ (α⊃α⊃α) ⊃α⊃αis deducible.## Example 6

CR_{α,α⊃α,α}VEQ_{α,α ⊃ α}: ⊢ (α⊃α⊃α) ⊃α⊃αmeant as

If we combine

CR_{α,α⊃α,α}andVEQ_{α,α ⊃ α}together viamodus ponens, then we get a proof that proves the following statement: (α⊃α⊃α) ⊃α⊃αis deducible.## Example 7

(

CR_{α,α⊃α,α}VEQ_{α,α ⊃ α})VEQ_{α,α}: ⊢α⊃αIf we combine the compund proof (

CR_{α,α⊃α,α}) together withVEQ_{α,α ⊃ α}(viamodus ponens), then we get an even more compund proof. This proves the following statement:α⊃αis deducible.## Combinatory logic

Although all this above has indeed provided a proof for the expected theorem, but it seems very unintuitive. It cannot be seen how people can "find out" the proof.

Let us see another field, where similar problems are investigated.

## Untyped combinatory logic

Combinatory logic can be regarded also as an extremely minimalistic functional programming language. Despite of its minimalism, it entirely Turing complete, but evenmore, one can write quite intuitive and complex programs even in this seemingly obfuscated language, in a modular and reusable way, with some practice gained from "normal" functional programming and some algebraic insights, .

## Adding typing rules

Combinatory logic also has typed variants. Syntax is augmented with types, and evenmore, in addition to reduction rules, also typing rules are added.

For base combinators:

K_{α,β}is selected as a basic combinator, inhabiting typeα→β→αS_{α,β,γ}is selected as a basic combinator, inhabiting type (α→β→γ) → (α→β) →α→γ.Typing rule of application:

Xinhabits typeα→βandYinhabits typeα, thenXYinhabits typeβ.## Notations and abbreviations

K_{α,β}:α→β→αS_{α,β,γ}: (α→β→γ) → (α→β)* →α→γ.X:α→βandY:α, thenXY:β.## Curry-Howard correspondence

It can be seen that the "patterns" are isomorphic in the proof calculus and in this typed combinatory logic.

Verum ex quolibetaxiom of the proof calculus corresponds to theKbase combinator of combinatory logicChain ruleaxiom of the proof calculus corresponds to theSbase combinator of combinatory logicModus ponensrule of inference in the proof calculus corresponds to the operation "application" in combinatory logic.## Functional programming

But what is the gain? Why should we translate problems to combinatory logic? I, personally, find it sometimes useful, because functional programming is a thing which has a large literature and is applied in practical problems. People can get used to it, when forced to use it in erveryday programming tasks ans pracice. And some tricks and hints of functional programming practice can be exploited very well in combinatory logic reductions. And if a "transferred" practice develops in combinatory logic, then it can be harnessed also in finding proofs in Hilbert system.

## External links

## Links how types in functional programming (lambda calculus, combinatory logic) can be translated into logical proofs and theorems:

Theorems for free!.## Links (or books) how to learn methods and practice to program directly in combinatory logic:

Combinatory Logic.Vol. I. Amsterdam: North-Holland Publishing Company.Binary Lambda Calculus and Combinatory Logic. Downloadable in PDF and Postscript from the author's John's Lambda Calculus and Combinatory Logic Playground.