ph |- ph is not an axiom by your definition, as it has the $e statement ph.
And Metamath doesn't even need to take that as an axiom, within its rules it can be proven without any previous theorems at all. just look at dummylink On Sun, Oct 20, 2019 at 8:27 AM 'fl' via Metamath <[email protected]> wrote: > > Kennington writes "But Lemmon used only deduction rules, with no axioms." > (1) I'm afraid > he didn't undertand what he read. It is perfectly impossible to have a > logical system > with no axiom. By axiom I mean a $a statement with no $e statement. > > It is often said that natural deduction has no axiom. But it is because > the rule > > Gamma, ph |- ph > > is implicit. (Where Gamma it the stack of hypotheses.) > > And this rule is an axiom even though the unique axiom of natural > deduction. > > (1) http://www.topology.org/tex/conc/diary.php?item=2019052201 > > -- > FL > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/2d18ac38-db8f-4981-b619-0552f5a7bcd8%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/2d18ac38-db8f-4981-b619-0552f5a7bcd8%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAB0L6P1DS3%2BEcznteTsM%2BvB24RUuf%2BZCPVy5_bNtzf%2BnFPcMRg%40mail.gmail.com.
