|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|