Page 306 of 800
| Page 306 of 800 | Search internet |
A construct is considered to be an object operator if it does not have a 'meta/kg' aspect. A term is an object term if it is a metavariable or an object operator applied to object terms. As an example, 
is an object term: 
and 
are object operators and 
is a meta variable.
A term is a statement (i.e. metaterm) if it is an object term or a meta operator applied to statements. As an example, 
is a metaterm. Metaquantifiers are required to bind over metavariables.
A term like 
is neither an object term, nor a statement.
For special cases (e.g. indexed variables, quotes, and the like), see the check page.
Metaquantifiers quantify over all statements for which its second argument is a statement. As an example, says 
for all object terms whereas 
says 
for all statements . If you only want to say for object terms you must include a side condition saying so.
In the Logiweb sequent calculus, axioms, inference rules, theories, theorems, lemmas, conjectures, and so on are expressed as statements. The calculus does not even distinguish between these categories.
| Page 306 of 800 | Search logiweb.eu |