Proof builder · Hilbert
Select two proof lines for modus ponens (Ctrl/⌘ + click).
Proof
Notation and instructions
Input accepts ¬, ∧, ∨, →, ↔ and ~, -, &, v, |, ->, =>, <->, <=>. Polish notation uses N, K, A, C, E.
Choose an axiom and enter substitutions, then press Axiom. To apply a definition, select it and one proof line, choose a proposed result and press Definition.
Language selection preserves the proof, selections, notation and unfinished input, including Setup drafts. Reloading or switching tools discards this working state; copy the proof before leaving.
Sie sind die You are visitor number 3378752. Besucherin.
Der Betrieb des Logikrechners kostet derzeit ca. 113,88€ pro Jahr (Cloudserver 85,07€, Domänengebühr 28,80€), deshalb hier ein Paypal-Spendenlink.
Operating the Logic server currently costs about 113.88€ per year (virtual server 85.07€, domain fee 28.80€); hence the Paypal donation link.