A logical system with no axiom

[fl]

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

[Sauer, Andrew Jacob]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2d18ac38-db8f-4981-b619-0552f5a7bcd8%40googlegroups.com.

[fl]

ph |- ph is not an axiom by your definition, as it has the $e statement ph.

Here "|-" is used loosely to separate the stack and the main statement. It belongs to a $a statement.

It is meaningful in a formalism where the stack is appended to the left of the main statement.

In full it would be:

hp $a [ Ga , ph ] |- ph

To separate $e statements and $p statements, I think metamath people use "&" and "=>". Look at the

theorems page for instances of this convention.

 

-- 

FL

[fl]

* It belongs to a $a statement.

-- 

FL

[fl]

*To separate $e statements from $p or $a statements,

 

-- 

FL

[fl]

Reflecting on Kennington's mistake, it became clear to me that in fact the notion of axiom is less obvious than it seems at first sight.

There is the case of stacks of systems such as natural deduction. After all, considering that the use as a premise of a statement on the stack is an axiom or not can be regarded as a matter of taste. But it has to be said that if we transform the stack into a context added to the left of the main proposal as in my previous post, well it becomes an axiom.

Then there are the syntax stories. They are not usually considered as axiom problems but there are two facts that show that the boundary is not clear either. First metamath manages the syntax as it manages the proofs by rewriting rules. Then an ambiguity in syntax can lead to a non-consistent system, as Mario Carneiro recently pointed out. The formula 2 - 1 -1 -1 = 2 - 1 - 1 - 1 can be interpreted as ( 2 - 1) - 1 = 2 - ( 1 - 1) and therefore giving 0 = 2 which of course breaks your system down. An ambiguous syntactic system ultimately has the same consequences as an inconsistent  system of axioms. 

Finally, there are the problems of provisos. Tarski showed that in a formalization with identity one can replace the substitutions normally made behind the scene by formulas and thus manage the substitutions in a transparent way in the proof itself

http://us.metamath.org/mpeuni/mmset.html#Tarski

Here again, the distinction between what belongs to axioms, theorems and proof and what belongs to the other elements of logic (management of a potential stack, syntax analysis, provisos checking, substitution algorithm) is imprecise.

Hence my conclusion that what is an axiom and what is not can be universally defined only in a very vague way and that in practice the concept depends on the type of system used.

-- 

FL

[fl]

Finally, there are the problems of provisos. Tarski showed that in a formalization with identity one can replace the substitutions normally made behind the scene by formulas and thus manage the substitutions in a transparent way in the proof itself

And we can also design a system with no distinct variables provisos at all. It would simply be totally unmanageable by human beings because the statements would

be cluttered by countless hypotheses of the " -. x = y" style.

 

[Ishan Murphy]

Just putting in my two cents, there are certain systems in which `ph, ps |- ps` is not a valid deduction; linear logic and relevance logic are examples. If you consider an axiom to be a Metamath $a statement with no logical hypotheses, then it would be impossible to prove any statement with no hypotheses without them, since no derivation would decrease the size of the proof stack.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d7e47217-b0c6-4091-b551-46d827fc4c7b%40googlegroups.com.