Page 100 of 800
| Page 100 of 800 | Search internet |
The Logiweb sequent calculus dictates that certain terms are definitely illformed. As an example, Logiweb sequent calculus does not like terms like 
because it embeds a metaquantifier inside an object term.
Apart from that, the Logiweb sequent calculus does not impose restrictions on terms. If you want to define a theory in which only certain terms are wellformed, then you will have to implement a check for wellformedness and you will have to add wellformedness side conditions to all your rules.
Peano arithmetic 
takes another approach: it considers all terms wellformed but only assign meaning to terms which are built up from object variables and constructors of . A term is an 'object variable' if it has no meta definition, no value definition, and no math definition, c.f. the definition of objectvar on the check page.
As an example, 
is no object variable since the pair operator has a value definition. Furthermore, does not make sense in Peano arithmetic. Thus, to Peano arithmetic, is a constant which denotes some, specific natural number, but Peano arithmetic does not care which one. To Peano arithmetic, could denote zero or 117 or a zillion of whatever. You can prove 
in Peano arithmetic if you like because any natural number equals itself, but you cannot do anything useful with in that theory.
When taking this approach it is important to ensure that the theory remains consistent. One can do that by ensuring that the resulting system has a model. As an example, one may assign the value zero to all formulas which are neither object variables nor something Peano arithmetic knows about.
One must also check what happens if one applies a quantifier to something which is not an object variable. One can typically interpret that situation as quantification over a fresh variable.
| Page 100 of 800 | Search logiweb.eu |