Editing Syntax (logic) (section)

==== Syntactic completeness of a formal system ====
{{Main|Completeness (logic)}}

A formal system <math> \mathcal{S}</math> is ''syntactically complete''<ref name="oxfordjournals">{{cite journal|url=http://jigpal.oxfordjournals.org/cgi/reprint/11/5/513.pdf|title=A Note on Interaction and Incompleteness|date=2003 |doi=10.1093/jigpal/11.5.513 |access-date=2014-10-15 |last1=Bojadziev |first1=D. |journal=Logic Journal of Igpl |volume=11 |issue=5 |pages=513–523 }}</ref><ref name="acm">{{cite journal|title=Normal forms and syntactic completeness proofs for functional independencies|year=2001|publisher=portal.acm.org|doi=10.1016/S0304-3975(00)00195-X|last1=Wijesekera|first1=Duminda|last2=Ganesh|first2=M.|last3=Srivastava|first3=Jaideep|last4=Nerode|first4=Anil|journal=Theoretical Computer Science|volume=266|issue=1–2|pages=365–405|doi-access=}}</ref><ref name="google4">{{cite book|title=Handbook of Mathematical Logic|author=Barwise, J.|author-link=Jon Barwise|date=1982|publisher=Elsevier Science|isbn=9780080933641|url=https://books.google.com/books?id=b0Fvrw9tBcMC|page=236|access-date=2014-10-15}}</ref><ref name="uniba2">{{cite web|url=http://www.swif.uniba.it/lei/foldop/foldoc.cgi?syntactic+completeness|archive-url=https://web.archive.org/web/20010502223539/http://www.swif.uniba.it/lei/foldop/foldoc.cgi?syntactic+completeness|url-status=dead|archive-date=2001-05-02|title=syntactic completeness from FOLDOC|publisher=swif.uniba.it|access-date=2014-10-15}}</ref> (also ''deductively complete'', ''maximally complete'', ''negation complete'' or simply ''complete'') iff for each formula A of the language of the system either A or ¬A is a theorem of <math> \mathcal{S}</math>. In another sense, a formal system is syntactically complete iff no unprovable axiom can be added to it as an axiom without introducing an [[consistency|inconsistency]]. Truth-functional [[propositional logic]] and first-order [[predicate logic]] are semantically complete, but not syntactically complete (for example the propositional logic statement consisting of a single variable "a" is not a theorem, and neither is its negation, but these are not [[tautology (logic)|tautologies]]). [[Gödel's incompleteness theorem]] shows that no [[recursive system]] that is sufficiently powerful, such as the [[Peano axioms]], can be both consistent and complete.