search

elexunix / qock

This project is currently an implementation of a proof-checker. But it is planned to be extended; for example, to support algorithm extraction from intuitionistic proofs, which is considered to be an interesting feature.
0 stars 0 forks source link

It's time to write the first proof #6

Closed elexunix closed 3 years ago

elexunix commented 3 years ago

I propose the following statement (for PA): every natural number is either even, or odd. That is, forall<variable, disjunction< exists<k, equal< variable, sum<variable, variable> >>, exists<k, equal< S<variable>, S<sum<variable, variable> >>

.

elexunix commented 3 years ago

(done)