|Page 355 of 800||Search internet|
The Logiweb sequent calculus is intuitionistic. One can build classical, intuitionistic, and other theories on top of it. And one can build meta-theories on top of the Logiweb sequent calculus and then build object theories on top of the meta-theories. You are invited to take any approach which fits your purposes.
The Logiweb sequent calculus is not constructed with the aim of reasoning inside it. If it were, it would contain more operators like operators for structural induction and for reasoning about side conditions. The intension of the Logiweb sequent calculus is to provide a low level machinery on which one can build arbitrary, high level theories.
|Page 355 of 800||Search logiweb.eu|