8.2.3 Statements

Prev Up Next 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, x + #x is an object term: x and "+" are object operators and #x 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, All #x : x and #x infer #x and x is a metaterm. Metaquantifiers are required to bind over metavariables.

A term like x + All #x : #x 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, All #x : x and #x infer #x and x says x and #x infer #x and x for all object terms #x whereas All #x : ( #y oplus #x ) infer ( #x oplus #y ) says ( #y oplus #x ) infer ( #x oplus #y ) for all statements #x. If you only want to say ( #y oplus #x ) infer ( #x oplus #y ) for object terms #x 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.

Prev Up Next Page 306 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05