Mercurial > cpdt > repo

comparison src/Universes.v @ 392:4b1242b277b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typo fixes
author Adam Chlipala <adam@chlipala.net>
date Fri, 20 Apr 2012 12:49:47 -0400
parents 057a29f9c773
children 05efde66559d
comparison
equal deleted inserted replaced
391:fd3f1057685c 392:4b1242b277b2
625 Axiom positive : n > 0. 625 Axiom positive : n > 0.
626 Reset n. 626 Reset n.
627 627
628 (** This kind of %``%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic. However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming. 628 (** This kind of %``%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic. However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming.
629 629
630 In general, there is a significant burden associated with any use of axioms. It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%. That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant. For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *) 630 In general, there is a significant burden associated with any use of axioms. It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%. That is, a set of axioms may imply [False], which allows any theorem to be proved, which defeats the purpose of a proof assistant. For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)
631 631
632 Axiom not_classic : ~ forall P : Prop, P \/ ~ P. 632 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.
633 633
634 Theorem uhoh : False. 634 Theorem uhoh : False.
635 generalize classic not_classic; tauto. 635 generalize classic not_classic; tauto.