yzchen/hilbert-axioms.md

Created August 2, 2019 19:25

Star (0) You must be signed in to star a gist
Fork (0) You must be signed in to fork a gist

Select an option

Learn more about clone URLs
Clone this repository at <script src="https://gist.github.com/yzchen/7cf98f2fac13606a69b366557650be0d.js"></script>
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

p -> (q -> p)

>p>qp
(p -> (q -> r)) -> ((p -> q) -> (p -> r))

>>p>qr>>pq>pr
(~q -> ~p) -> (p -> q)

>>~q~p>pq
p -> (~p -> q)

>p>~pq
(~p -> p) -> p

>>~ppp

Modus Ponens

((p -> q) ∧ p) -> q

>&>pqpq

Hilbert L1 Axioms

(∀x p) -> p[x/t]
(∀x (p -> q)) -> (∀x p -> ∀x q)
p -> ∀x p

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