Skip to content

Instantly share code, notes, and snippets.

@yzchen

yzchen/hilbert-axioms.md

Created August 2, 2019 19:25
Show Gist options
  • Save yzchen/7cf98f2fac13606a69b366557650be0d to your computer and use it in GitHub Desktop.
Save yzchen/7cf98f2fac13606a69b366557650be0d to your computer and use it in GitHub Desktop.
Download ZIP
希尔伯特公理
Raw
hilbert-axioms.md

Hilbert Axioms

Notes :

  • > : implication, ->

  • ~ : not, ¬

  • & : and, ∧

  • | : or, ∨

Axioms

  1. p -> (q -> p)

    >p>qp

  2. (p -> (q -> r)) -> ((p -> q) -> (p -> r))

    >>p>qr>>pq>pr

  3. (~q -> ~p) -> (p -> q)

    >>~q~p>pq

  4. p -> (~p -> q)

    >p>~pq

  5. (~p -> p) -> p

    >>~ppp

Modus Ponens

  1. ((p -> q) ∧ p) -> q

    >&>pqpq

Hilbert L1 Axioms

  1. (∀x p) -> p[x/t]

  2. (∀x (p -> q)) -> (∀x p -> ∀x q)

  3. p -> ∀x p

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment