Editing Syntax (logic) (section)

=== Formal systems ===
{{main|Formal system}}

A ''formal system'' (also called a ''logical calculus'', or a ''logical system'') consists of a formal language together with a [[deductive apparatus]] (also called a ''deductive system''). The deductive apparatus may consist of a set of [[transformation rule]]s (also called ''inference rules'') or a set of [[axiom]]s, or have both. A formal system is used to derive one expression from one or more other expressions. Formal systems, like other syntactic entities may be defined without any [[Interpretation (logic)|interpretation]] given to it (as being, for instance, a system of arithmetic).

==== Syntactic consequence within a formal system ====

A formula A is a '''syntactic consequence'''<ref name="google">{{cite book|title=Frege: Philosophy of Language|author=Dummett, M.|date=1981|publisher=Harvard University Press|isbn=9780674319318|url=https://books.google.com/books?id=EYP7uCZIRQYC|page=82|access-date=2014-10-15}}</ref><ref name="google2">{{cite book|title=Aristotle and Logical Theory|author=Lear, J.|date=1986|publisher=Cambridge University Press|isbn=9780521311786|url=https://books.google.com/books?id=lXI7AAAAIAAJ|page=1|access-date=2014-10-15}}</ref><ref name="google3">{{cite book|title=The Cambridge Companion to Carnap|author1=Creath, R.|author2=Friedman, M.|date=2007|publisher=Cambridge University Press|isbn=9780521840156|url=https://books.google.com/books?id=87BcFLgJmxMC|page=189|access-date=2014-10-15}}</ref><ref name="uniba">{{cite web|url=http://www.swif.uniba.it/lei/foldop/foldoc.cgi?syntactic+consequence|title=syntactic consequence from FOLDOC|publisher=swif.uniba.it|access-date=2014-10-15|url-status=dead|archive-url=https://web.archive.org/web/20130403201417/http://www.swif.uniba.it/lei/foldop/foldoc.cgi?syntactic+consequence|archive-date=2013-04-03}}</ref> within some formal system <math> \mathcal{FS}</math> of a set Г of formulas if there is a [[Formal proof|derivation]] in [[formal system]] <math> \mathcal{FS}</math> of A from the set Г.

:<math>\Gamma \vdash_{\mathrm FS} A</math>

Syntactic consequence does not depend on any [[interpretation (logic)|interpretation]] of the formal system.<ref>Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Press, 1971, p. 75.</ref>

==== 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.