Prototype / Predicate Calculus
Based on the results of the propositional calculus here are predicate calculus theorems derived.
The following documents were generated again with the prototype out of qedeq modules. The qedeq modules were checked for formal correctness with the integrated proof verifier. (Also see last column.)
If the viewing of the HTML pages in the first column is not satisfactorily please try the second HTML links (o.html) which require an installed symbol font. If you have also trouble viewing these HTML pages please take look at Ian Hutchinson's pages: Browser Problems and Comparative Review of WorldWideWeb Mathematics Renderers.
Basic definitions of predicate logic
lang&rules 

html 
o.html 




informal definition of the used language and the rules of derivation 
predaxiom 

html 
o.html 
pdf 
tex 
qedeq 

additional axioms, and declarations of the rules of derivation of predicate calculus 
Simple derivations
With meta rules
The following variant of predtheo2 uses meta rules from rule version 1.02.00.
