Timeline for Proof of Lindenbaum lemma without deduction theorem
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 7 at 20:58 | comment | added | paulotorrens | Hilbert style. I'm assuming the system has at least ten propositional axioms (including the two classical I mentioned above), plus K and possibility (modal). Those are listed in here: github.com/funcao/LML/blob/completeness/coq/… (1 to 10, K, pos). It has modus poenens, but the deduction theorem is not derivable. | |
| Mar 7 at 20:52 | comment | added | Andrej Bauer | Is it a Hilbert-style system or natural deduction? | |
| Mar 7 at 20:19 | comment | added | paulotorrens | Indeed, if I have point 3 you mention this can be done. The system is indeed classic, as it has (as axioms) that $(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)$ and that $\neg\neg\phi\rightarrow\phi$. Still, I'm not sure how to go from that into your point 3 without the deduction theorem. That's precisely where I'm stuck. | |
| Mar 7 at 20:03 | history | answered | Andrej Bauer | CC BY-SA 4.0 |