5199:
2662:
2689:
of operands. In computer algebra software, the expressions are usually represented in this way. This representation is very flexible, and many things that seem not to be mathematical expressions at first glance, may be represented and manipulated as such. For example, an equation is an expression
1438:
The semantic rules may declare that certain expressions do not designate any value (for instance when they involve division by 0); such expressions are said to have an undefined value, but they are well-formed expressions nonetheless. In general the meaning of expressions is not limited to
1443:
that is to be solved, or it can be viewed as an object in its own right that can be manipulated according to certain rules. Certain expressions that designate a value simultaneously express a condition that is assumed to hold, for instance those involving the operator
734:
876:
903:
For a given combination of values for the free variables, an expression may be evaluated, although for some combinations of values of the free variables, the value of the expression may be undefined. Thus an expression represents an
1037:
Two expressions are said to be equivalent if, for each combination of values for the free variables, they have the same output, i.e., they represent the same function. The equivalence between two expressions is called an
1291:
1819:
2327:
3394:
1743:
1205:
1021:
579:
1553:
2173:. This is also the case for the expressions representing real numbers, which are built from the integers by using the arithmetical operations, the logarithm and the exponential (
1961:
1890:
1593:
that can be performed on elements over the domain, like addition (+), multiplication (Ă), or set operations like union (âȘ), or intersection (â©). (Functions can be understood as
1121:
2925:
513:
286:
3578:
2487:
2411:
1384:
2604:, formulas are viewed as expressions that can be evaluated as a Boolean, depending on the values that are given to the variables occurring in the expressions. For example
2111:
334:
2813:
2079:
599:
191:
2637:
148:
4253:
2048:
1063:
1462:
1930:
2491:
Many author do not distinguish polynomials and polynomial expressions. In this case the expression of a polynomial expression as a linear combination is called the
2024:
452:
217:
113:
937:
738:
416:
237:
2865:
2841:
2004:
1910:
1846:
1677:
1652:
1632:
4336:
3477:
3433:
4650:
2435:
of products of integer powers of the indeterminates. For example the above polynomial expression is equivalent (denote the same polynomial as
4808:
3224:
3152:
3037:
2724:. A term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula.
1423:
attached to the symbols of the expression. The choice of semantics depends on the context of the expression. The same syntactic expression
3596:
1217:
4663:
3986:
3202:
Pratt, Vaughan, "Algebra", The
Stanford Encyclopedia of Philosophy (Winter 2022 Edition), Edward N. Zalta & Uri Nodelman (eds.), URL:
3113:
349:
4248:
4668:
4658:
4395:
3601:
4146:
3592:
1145:
4804:
1325:
must have the correct number of inputs in the correct places, the characters that make up these inputs must be valid, have a clear
3088:
4901:
4645:
3470:
4206:
3899:
3640:
5162:
4864:
4627:
4622:
4447:
3868:
3552:
3275:
2526:
3142:
249:, or inputs, of the function, and assigning the output to be the total evaluation of the resulting expression. For example,
1329:, etc. Strings of symbols that violate the rules of syntax are not well-formed and are not valid mathematical expressions.
5157:
4940:
4857:
4570:
4501:
4378:
3620:
2512:
4228:
1753:
379:
equal, that is, if they are the exact same expression. For instance, the formal expressions "2" and "1+1" are not equal.
5228:
5082:
4908:
4594:
3827:
2655:
2273:
4233:
5233:
4565:
4304:
3562:
3463:
2670:
2163:
1686:
1488:
4960:
4955:
1966:
Brackets are initially around each non-atomic expression, but they can be deleted in cases where there is a defined
956:
4889:
4479:
3873:
3841:
3532:
2586:
3606:
371:
as standard expressions, however, they are used without regard to the meaning of the expression. In this way, two
5223:
5179:
5128:
5025:
4523:
4484:
3961:
3014:
2578:
530:
360:
78:, and the latter denoting a statement about mathematical objects. This is analogous to natural language, where a
5020:
3635:
4950:
4489:
4341:
4047:
3527:
3379:
Maurizio
Gabbrielli, Simone Martini (2010). Programming Languages - Principles and Paradigms. Springer London,
2562:
2534:
2359:, and the operators of addition, multiplication, and exponentiation to nonnegative integer powers; for example
2356:
1403:
2113:
have exactly one. There are countably infinitely many WFE's, however, each WFE has a finite number of nodes.
3441:
4852:
4829:
4790:
4676:
4617:
4263:
4183:
4027:
3971:
3584:
2987:
2736:
2174:
1983:
1590:
1514:
905:
50:
5142:
4869:
4847:
4814:
4707:
4553:
4538:
4511:
4462:
4346:
4281:
4106:
4072:
4067:
3941:
3772:
3749:
2967:
2952:
2760:
2756:
2682:
2550:
2546:
2542:
2538:
2221:
2201:
2147:
1569:
1416:
1322:
1039:
889:
246:
242:
83:
54:
46:
42:
3191:
1935:
1855:
5072:
4925:
4717:
4435:
4171:
4077:
3936:
3921:
3802:
3777:
3418:
For a full history, see
Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
3396:
The
Feasibility of Automatic Storage Reclamation with Concurrent Program Execution in a LISP Environment
2962:
2590:
2348:
62:
38:
5198:
2874:
1070:
469:
252:
5045:
5007:
4884:
4688:
4528:
4452:
4430:
4258:
4216:
4115:
4082:
3946:
3734:
3645:
2732:
2691:
2558:
2530:
2438:
2352:
2192:
1979:
1971:
1481:
516:
70:
30:
2537:
or fail to terminate, in which case the expression is undefined. It is a combination of one or more
2362:
1346:
729:{\displaystyle f(a)+\sum _{k=1}^{n}\left.{\frac {1}{k!}}{\frac {d^{k}}{dt^{k}}}\right|_{t=0}f(u(t))}
5174:
5065:
5050:
5030:
4987:
4874:
4824:
4750:
4695:
4632:
4425:
4420:
4368:
4136:
4125:
3797:
3697:
3625:
3616:
3612:
3547:
3542:
2947:
2721:
2574:
2554:
2205:
1967:
1500:
1496:
1432:
1428:
1326:
1318:
75:
291:
5203:
4972:
4935:
4920:
4913:
4896:
4682:
4548:
4474:
4457:
4410:
4223:
4132:
3966:
3951:
3911:
3863:
3848:
3836:
3792:
3767:
3537:
3486:
3320:
3080:
2768:
2709:
2582:
2432:
2333:
2159:
2084:
1606:
With this alphabet, the recursive rules for forming well-formed expression (WFE) are as follows:
164:
4700:
4156:
2607:
2053:
118:
65:(often used for grouping, that is for considering a part of the expression as a single symbol).
1408:
Semantics is the study of meaning. Formal semantics is about attaching meaning to expressions.
5138:
4945:
4755:
4745:
4637:
4518:
4353:
4329:
4110:
4094:
3999:
3976:
3853:
3822:
3787:
3682:
3517:
3281:
3271:
3244:
3220:
3172:
3148:
3123:
3033:
2982:
2740:
2728:
2594:
2337:
1508:
1045:
582:
455:
341:
3347:
2029:
1447:
908:
over constants and free variables and whose output is the resulting value of the expression.
5152:
5147:
5040:
4997:
4819:
4780:
4775:
4760:
4586:
4543:
4440:
4238:
4188:
3762:
3724:
3363:
3312:
3240:
3168:
3119:
3072:
2698:
2601:
2518:
2197:
2170:
1915:
1849:
1594:
1586:
1026:
871:{\displaystyle +\int _{0}^{1}{\frac {(1-t)^{n}}{n!}}{\frac {d^{n+1}}{dt^{n+1}}}f(u(t))\,dt.}
2694:
may be represented as an expression with "matrix" as an operator and its rows as operands.
2009:
1415:, an expression may be used to designate a value, which might depend on values assigned to
161:
by replacing operations that appear in them with their result. For example, the expression
5133:
5123:
5077:
5060:
5015:
4977:
4879:
4799:
4606:
4533:
4506:
4494:
4400:
4314:
4288:
4243:
4211:
4012:
3814:
3757:
3707:
3672:
3630:
2977:
2229:
2151:
2135:
2122:
1680:
1477:
428:
364:
337:
196:
89:
2685:, every mathematical expression may be viewed as the symbol of an operator followed by a
914:
395:
222:
3057:
5118:
5097:
5055:
5035:
4930:
4785:
4383:
4373:
4363:
4358:
4292:
4166:
4042:
3931:
3926:
3904:
3505:
2850:
2826:
2744:
2424:
2225:
2217:
2143:
1989:
1895:
1831:
1662:
1637:
1617:
1611:
1312:
1301:
897:
376:
34:
5217:
5092:
4770:
4277:
4062:
4052:
4022:
4007:
3677:
3340:
3300:
3084:
3053:
2752:
2420:
2416:
2155:
2139:
2128:
1565:
893:
4992:
4839:
4740:
4732:
4612:
4560:
4469:
4405:
4388:
4319:
4178:
4037:
3739:
3522:
3203:
2717:
1556:
1439:
designating values; for instance, an expression might designate a condition, or an
3366:(2002). Concepts in Programming Languages. Cambridge: Cambridge University Press,
3251:. Studies in Logic and the Foundation of Mathematics. Vol. 73. North Holland.
3179:. Studies in Logic and the Foundation of Mathematics. Vol. 73. North Holland.
2565:
environment) another value. This process, for mathematical expressions, is called
3402:(Master's thesis). Naval Postgraduate School, Monterey/CA. p. 15. ADA165184.
5102:
4982:
4161:
4151:
4098:
3782:
3702:
3687:
3567:
3512:
3263:
2930:
2570:
2248:
2213:
1825:
1572:
used for representing mathematical objects in the domain. (Usually letters like
79:
58:
22:
2661:
4032:
3887:
3858:
3664:
2957:
2428:
1465:
1333:
3285:
5184:
5087:
4140:
4057:
4017:
3981:
3917:
3729:
3719:
3692:
2972:
1420:
1419:
occurring in the expression. The determination of this value depends on the
1399:
1427:
can have different values (mathematically 7, but also 9), depending on the
3076:
5169:
4967:
4415:
4120:
3714:
3008:
2686:
2209:
1440:
4765:
3557:
3324:
1504:
1412:
3192:
http://encyclopediaofmath.org/index.php?title=Equation&oldid=32613
2553:
that the programming language interprets (according to its particular
1476:
A well-formed expression in mathematics can be described as part of a
3455:
2678:
3316:
16:
A finite combination of symbols that describes a mathematical object
4309:
3655:
3500:
2748:
1321:. It can be described somewhat informally as follows: the allowed
1135:
is free. This expression is equivalent to the simpler expression
3127:
348:
if they define the same function. Such an equality is called a "
3459:
352:
equality", that is, both expressions "mean the same thing."
3303:(1932). "A set of postulates for the foundation of logic".
1970:, or where order doesn't matter (i.e. where operations are
1495:
A set of
Constants / Definites: Symbols representing fixed
641:
2658:âsyntactic entities that have no value (an instruction).
340:
plus one. An expression with no variables would define a
3058:"A Relational Model of Data for Large Shared Data Banks"
336:
define the function that associates to each number its
2087:
2056:
2032:
1286:{\displaystyle \sum _{n=1}^{3}(2nx){\Big |}_{x=3}=36.}
1073:
2877:
2853:
2829:
2771:
2610:
2441:
2365:
2276:
2012:
1992:
1938:
1918:
1898:
1858:
1834:
1756:
1689:
1665:
1640:
1620:
1614:(the simplest WFE's). For instance, the expressions "
1517:
1450:
1349:
1220:
1148:
1048:
959:
917:
741:
602:
533:
472:
431:
398:
294:
255:
225:
199:
167:
121:
92:
5111:
5006:
4838:
4731:
4583:
4276:
4199:
4093:
3997:
3886:
3813:
3748:
3663:
3654:
3576:
3493:
3342:
Academic Press dictionary of science and technology
1814:{\displaystyle F(\phi _{1},\phi _{2},...\phi _{n})}
1317:An expression is a syntactic construct. It must be
892:. Any variable can be classified as being either a
344:. Usually, two expressions are considered equal or
3339:
2919:
2859:
2835:
2817:is a term built from the constant 1, the variable
2807:
2631:
2481:
2405:
2322:{\displaystyle {\sqrt {\frac {1-x^{2}}{1+x^{2}}}}}
2321:
2105:
2073:
2042:
2018:
1998:
1955:
1924:
1904:
1884:
1840:
1813:
1737:
1671:
1646:
1626:
1547:
1456:
1378:
1285:
1199:
1115:
1057:
1015:
931:
870:
728:
573:
507:
446:
410:
328:
280:
231:
211:
185:
142:
107:
2427:, every polynomial expression is equivalent to a
2267:, the following is also an algebraic expression:
1260:
3204:https://plato.stanford.edu/entries/algebra/#Laws
2134:In the 1930s, a new type of expressions, called
1738:{\displaystyle \phi _{1},\phi _{2},...\phi _{n}}
2743:to an appropriate number of terms is called an
2150:and their evaluation. They form the basis for
2026:have exactly two child nodes, while operations
1824:For instance, if the domain of discorse is the
1200:{\displaystyle \sum _{n=1}^{3}(2nx)\equiv 12x.}
387:The use of expressions ranges from the simple:
1016:{\displaystyle x/y{\text{ }}|_{x=10,\,y=5}=2.}
68:Many authors distinguish an expression from a
3471:
2561:) and computes to produce ("to return", in a
2247:is an algebraic expression. Since taking the
2169:The equivalence of two lambda expressions is
1978:A well-formed expression can be thought as a
8:
3190:Equation. Encyclopedia of Mathematics. URL:
2647:is given a value less than 1, and the value
1610:Any constant or variable as defined are the
1542:
1524:
574:{\displaystyle {\frac {x-1}{{{x}^{2}}+12}}}
4297:
3892:
3660:
3478:
3464:
3456:
1986:are always atomic expressions. Operations
3219:. San Francisco, CA: Dover Publications.
3032:. San Francisco, CA: Dover Publications.
2876:
2852:
2828:
2770:
2609:
2449:
2440:
2385:
2364:
2309:
2291:
2277:
2275:
2088:
2086:
2057:
2055:
2033:
2031:
2011:
1991:
1945:
1939:
1937:
1917:
1897:
1876:
1863:
1857:
1833:
1802:
1780:
1767:
1755:
1729:
1707:
1694:
1688:
1664:
1639:
1619:
1516:
1449:
1368:
1348:
1265:
1259:
1258:
1236:
1225:
1219:
1164:
1153:
1147:
1089:
1078:
1072:
1047:
995:
982:
977:
971:
963:
958:
921:
916:
858:
822:
802:
796:
779:
760:
754:
749:
740:
693:
679:
665:
659:
644:
633:
622:
601:
555:
550:
548:
534:
532:
483:
478:
476:
471:
430:
397:
314:
293:
266:
254:
224:
198:
166:
120:
91:
3346:. Gulf Professional Publishing. p.
2660:
2131:the concept of well-formed expressions.
1654:" are syntactically correct expressions.
241:An expression is often used to define a
3411:
3000:
2533:that may be evaluated to determine its
1518:
2735:from constant symbols, variables, and
2654:Expressions are often contrasted with
1548:{\displaystyle \varnothing ,\{1,2,3\}}
375:are considered equal only if they are
368:
2739:. An expression formed by applying a
2355:(numbers of elements of some field),
950:, it evaluates to 2; this is denoted
7:
2251:is the same as raising to the power
2869:; it is part of the atomic formula
1956:{\displaystyle {\sqrt {\phi _{1}}}}
1885:{\displaystyle \phi _{1}+\phi _{2}}
3352:algebraic expression over a field.
3268:Introduction to Mathematical Logic
3144:A first course in abstract algebra
2821:, and the binary function symbols
2431:, that is an expression that is a
1116:{\textstyle \sum _{n=1}^{3}(2nx),}
14:
2929:which evaluates to true for each
2920:{\displaystyle (x+1)*(x+1)\geq 0}
2673:tree, from a 1985 Master's Thesis
2665:Representation of the expression
1431:implied by the context (See also
82:refers to an object, and a whole
33:following the context-dependent,
5197:
3368:3.4.1 Statements and Expressions
3147:. Boston : Addison-Wesley.
508:{\displaystyle 7{{x}^{2}}+4x-10}
281:{\displaystyle x\mapsto x^{2}+1}
245:, by taking the variables to be
3338:Morris, Christopher G. (1992).
3094:from the original on 2004-09-08
2482:{\displaystyle 3x^{2}-xy+6x+3.}
2196:is an expression built up from
2164:theory of programming languages
1745:be metavariables for any WFE's.
1067:For example, in the expression
911:For example, if the expression
86:refers to a fact. For example,
41:. Symbols can denote numbers (
3393:Cassidy, Kevin G. (Dec 1985).
3115:Introduction To Modern Algebra
3010:âexpression (n.), sense II.7,â
2908:
2896:
2890:
2878:
2802:
2790:
2784:
2772:
2406:{\displaystyle 3(x+1)^{2}-xy.}
2382:
2369:
2068:
2062:
1919:
1808:
1760:
1379:{\displaystyle \times 4)x+,/y}
1356:
1254:
1242:
1182:
1170:
1107:
1095:
978:
855:
852:
846:
840:
776:
763:
723:
720:
714:
708:
612:
606:
304:
298:
259:
1:
5158:History of mathematical logic
2513:Expression (computer science)
5083:Primitive recursive function
2351:is an expression built with
2106:{\textstyle {\frac {d}{dx}}}
1214:is 36, which can be denoted
1129:is bound, and the variable
329:{\displaystyle f(x)=x^{2}+1}
29:is a written arrangement of
2808:{\displaystyle (x+1)*(x+1)}
2699:Computer algebra expression
2690:with "=" as an operator, a
2074:{\textstyle {\text{ln}}(x)}
1912:can be the unary operation
1564:A set of variable names: A
186:{\displaystyle 8\times 2-5}
5250:
4147:SchröderâBernstein theorem
3874:Monadic predicate calculus
3533:Foundations of mathematics
3141:Fraleigh, John B. (2003).
2632:{\displaystyle 8x-5\geq 3}
2573:is usually one of various
2569:. In simple settings, the
2510:
2120:
1397:
1310:
1299:
1042:and is often denoted with
143:{\displaystyle 8x-5\geq 3}
5193:
5180:Philosophy of mathematics
5129:Automated theorem proving
4300:
4254:Von NeumannâBernaysâGödel
3895:
3065:Communications of the ACM
3015:Oxford English Dictionary
1683:over the domain, and let
1464:to designate an internal
888:Many expressions include
2585:, or numerical (such as
2507:Computational expression
2043:{\textstyle {\sqrt {x}}}
1433:Operations § Calculators
1404:Formal semantics (logic)
1058:{\displaystyle \equiv .}
884:Variables and evaluation
115:is an expression, while
74:, the former denoting a
57:. Other symbols include
4830:Self-verifying theories
4651:Tarski's axiomatization
3602:Tarski's undefinability
3597:incompleteness theorems
3112:McCoy, Neal H. (1960).
2988:Well-defined expression
2733:recursively constructed
2127:Formal languages allow
1457:{\displaystyle \oplus }
1296:Syntax versus semantics
193:evaluates partially to
5204:Mathematics portal
4815:Proof of impossibility
4463:propositional variable
3773:Propositional calculus
2968:Functional programming
2953:Closed-form expression
2921:
2861:
2837:
2809:
2674:
2633:
2483:
2407:
2323:
2107:
2075:
2044:
2020:
2000:
1957:
1926:
1925:{\displaystyle \surd }
1906:
1886:
1842:
1815:
1739:
1673:
1648:
1628:
1549:
1458:
1380:
1287:
1241:
1201:
1169:
1117:
1094:
1059:
1017:
933:
872:
730:
638:
575:
509:
448:
412:
367:, created by the same
330:
282:
233:
213:
187:
144:
109:
5073:Kolmogorov complexity
5026:Computably enumerable
4926:Model complete theory
4718:Principia Mathematica
3778:Propositional formula
3607:BanachâTarski paradox
3432:Redden, John (2011).
3305:Annals of Mathematics
3077:10.1145/362384.362685
2963:Defined and undefined
2922:
2862:
2838:
2810:
2747:, which evaluates to
2664:
2634:
2484:
2408:
2349:polynomial expression
2343:Polynomial expression
2324:
2138:, were introduced by
2108:
2076:
2045:
2021:
2019:{\displaystyle \cup }
2001:
1958:
1927:
1907:
1887:
1843:
1816:
1740:
1674:
1649:
1629:
1585:A set of operations:
1550:
1459:
1381:
1340:is well-formed, but
1288:
1221:
1202:
1149:
1118:
1074:
1060:
1018:
934:
873:
731:
618:
576:
510:
449:
413:
331:
283:
234:
214:
188:
145:
110:
39:mathematical notation
5021:ChurchâTuring thesis
5008:Computability theory
4217:continuum hypothesis
3735:Square of opposition
3593:Gödel's completeness
3438:Flat World Knowledge
3434:"Elementary Algebra"
3217:Set Theory and Logic
3030:Set Theory and Logic
2875:
2851:
2827:
2769:
2716:can refer to either
2714:"logical expression"
2608:
2531:programming language
2439:
2363:
2274:
2206:algebraic operations
2193:algebraic expression
2186:Algebraic expression
2181:Types of expressions
2175:Richardson's theorem
2085:
2054:
2030:
2010:
1990:
1936:
1916:
1896:
1856:
1832:
1754:
1687:
1663:
1638:
1618:
1515:
1507:(1, 2.5, 1/7, ...),
1448:
1347:
1218:
1146:
1071:
1046:
957:
915:
739:
600:
531:
517:quadratic polynomial
470:
447:{\displaystyle 8x-5}
429:
396:
292:
253:
223:
212:{\displaystyle 16-5}
197:
165:
119:
108:{\displaystyle 8x-5}
90:
5229:Logical expressions
5175:Mathematical object
5066:P versus NP problem
5031:Computable function
4825:Reverse mathematics
4751:Logical consequence
4628:primitive recursive
4623:elementary function
4396:Free/bound variable
4249:TarskiâGrothendieck
3768:Logical connectives
3698:Logical equivalence
3548:Logical consequence
3290:; here: Sect.II.1.3
3270:. Springer London.
2948:Analytic expression
2555:rules of precedence
2503:of the polynomial.
2198:algebraic constants
1968:order of operations
1501:domain of discourse
1482:defined recursively
1429:order of operations
1327:order of operations
932:{\displaystyle x/y}
759:
411:{\displaystyle 3+8}
232:{\displaystyle 11.}
159:partially evaluated
153:Expressions can be
76:mathematical object
5234:Elementary algebra
4973:Transfer principle
4936:Semantics of logic
4921:Categorical theory
4897:Non-standard model
4411:Logical connective
3538:Information theory
3487:Mathematical logic
2917:
2857:
2833:
2805:
2710:mathematical logic
2704:Logical expression
2675:
2629:
2479:
2433:linear combination
2403:
2334:Algebraic equation
2319:
2160:mathematical logic
2136:lambda expressions
2103:
2071:
2040:
2016:
1996:
1953:
1922:
1902:
1882:
1838:
1811:
1735:
1669:
1644:
1624:
1612:atomic expressions
1566:countably infinite
1545:
1454:
1376:
1283:
1197:
1113:
1055:
1025:The evaluation is
1013:
939:is evaluated with
929:
868:
745:
726:
571:
505:
444:
408:
373:formal expressions
326:
278:
229:
209:
183:
140:
105:
5211:
5210:
5143:Abstract category
4946:Theories of truth
4756:Rule of inference
4746:Natural deduction
4727:
4726:
4272:
4271:
3977:Cartesian product
3882:
3881:
3788:Many-valued logic
3763:Boolean functions
3646:Russell's paradox
3621:diagonal argument
3518:First-order logic
3245:H. Jerome Keisler
3226:978-0-486-63829-4
3215:Stoll, Robert R.
3173:H. Jerome Keisler
3154:978-0-201-76390-4
3120:Allyn & Bacon
3054:Codd, Edgar Frank
3039:978-0-486-63829-4
3028:Stoll, Robert R.
2983:Signature (logic)
2860:{\displaystyle *}
2836:{\displaystyle +}
2667:(8 â 6) Ă (3 + 1)
2338:Algebraic closure
2317:
2316:
2101:
2060:
2038:
1999:{\displaystyle +}
1951:
1905:{\displaystyle F}
1841:{\displaystyle F}
1672:{\displaystyle F}
1647:{\displaystyle x}
1627:{\displaystyle 2}
1472:Formal definition
1336:, the expression
974:
835:
794:
686:
657:
591:to the complex:
583:rational fraction
569:
456:linear polynomial
357:formal expression
342:constant function
5241:
5224:Abstract algebra
5202:
5201:
5153:History of logic
5148:Category of sets
5041:Decision problem
4820:Ordinal analysis
4761:Sequent calculus
4659:Boolean algebras
4599:
4598:
4573:
4544:logical/constant
4298:
4284:
4207:ZermeloâFraenkel
3958:Set operations:
3893:
3830:
3661:
3641:LöwenheimâSkolem
3528:Formal semantics
3480:
3473:
3466:
3457:
3452:
3450:
3449:
3440:. Archived from
3419:
3416:
3404:
3403:
3401:
3390:
3384:
3377:
3371:
3361:
3355:
3354:
3345:
3335:
3329:
3328:
3297:
3291:
3289:
3260:
3254:
3253:; here: Sect.1.3
3252:
3237:
3231:
3230:
3212:
3206:
3200:
3194:
3188:
3182:
3181:; here: Sect.1.3
3180:
3165:
3159:
3158:
3138:
3132:
3131:
3109:
3103:
3102:
3100:
3099:
3093:
3062:
3050:
3044:
3043:
3025:
3019:
3018:
3005:
2936:
2928:
2926:
2924:
2923:
2918:
2868:
2866:
2864:
2863:
2858:
2844:
2842:
2840:
2839:
2834:
2820:
2816:
2814:
2812:
2811:
2806:
2741:predicate symbol
2737:function symbols
2668:
2646:
2639:takes the value
2638:
2636:
2635:
2630:
2602:computer algebra
2519:computer science
2488:
2486:
2485:
2480:
2454:
2453:
2412:
2410:
2409:
2404:
2390:
2389:
2328:
2326:
2325:
2320:
2318:
2315:
2314:
2313:
2297:
2296:
2295:
2279:
2278:
2266:
2264:
2263:
2260:
2257:
2246:
2232:). For example,
2146:for formalizing
2112:
2110:
2109:
2104:
2102:
2100:
2089:
2080:
2078:
2077:
2072:
2061:
2058:
2049:
2047:
2046:
2041:
2039:
2034:
2025:
2023:
2022:
2017:
2005:
2003:
2002:
1997:
1962:
1960:
1959:
1954:
1952:
1950:
1949:
1940:
1931:
1929:
1928:
1923:
1911:
1909:
1908:
1903:
1891:
1889:
1888:
1883:
1881:
1880:
1868:
1867:
1850:binary operation
1847:
1845:
1844:
1839:
1820:
1818:
1817:
1812:
1807:
1806:
1785:
1784:
1772:
1771:
1744:
1742:
1741:
1736:
1734:
1733:
1712:
1711:
1699:
1698:
1678:
1676:
1675:
1670:
1653:
1651:
1650:
1645:
1633:
1631:
1630:
1625:
1595:unary operations
1587:Function symbols
1579:
1575:
1554:
1552:
1551:
1546:
1463:
1461:
1460:
1455:
1385:
1383:
1382:
1377:
1372:
1332:For example, in
1292:
1290:
1289:
1284:
1276:
1275:
1264:
1263:
1240:
1235:
1213:
1206:
1204:
1203:
1198:
1168:
1163:
1141:
1134:
1128:
1122:
1120:
1119:
1114:
1093:
1088:
1064:
1062:
1061:
1056:
1022:
1020:
1019:
1014:
1006:
1005:
981:
975:
972:
967:
949:
938:
936:
935:
930:
925:
877:
875:
874:
869:
836:
834:
833:
832:
813:
812:
797:
795:
793:
785:
784:
783:
761:
758:
753:
735:
733:
732:
727:
704:
703:
692:
688:
687:
685:
684:
683:
670:
669:
660:
658:
656:
645:
637:
632:
580:
578:
577:
572:
570:
568:
561:
560:
559:
554:
546:
535:
514:
512:
511:
506:
489:
488:
487:
482:
453:
451:
450:
445:
417:
415:
414:
409:
369:production rules
335:
333:
332:
327:
319:
318:
287:
285:
284:
279:
271:
270:
238:
236:
235:
230:
218:
216:
215:
210:
192:
190:
189:
184:
149:
147:
146:
141:
114:
112:
111:
106:
5249:
5248:
5244:
5243:
5242:
5240:
5239:
5238:
5214:
5213:
5212:
5207:
5196:
5189:
5134:Category theory
5124:Algebraic logic
5107:
5078:Lambda calculus
5016:Church encoding
5002:
4978:Truth predicate
4834:
4800:Complete theory
4723:
4592:
4588:
4584:
4579:
4571:
4291: and
4287:
4282:
4268:
4244:New Foundations
4212:axiom of choice
4195:
4157:Gödel numbering
4097: and
4089:
3993:
3878:
3828:
3809:
3758:Boolean algebra
3744:
3708:Equiconsistency
3673:Classical logic
3650:
3631:Halting problem
3619: and
3595: and
3583: and
3582:
3577:Theorems (
3572:
3489:
3484:
3447:
3445:
3431:
3428:
3423:
3422:
3417:
3413:
3408:
3407:
3399:
3392:
3391:
3387:
3381:6.1 Expressions
3378:
3374:
3362:
3358:
3337:
3336:
3332:
3317:10.2307/1968337
3299:
3298:
3294:
3278:
3262:
3261:
3257:
3239:
3238:
3234:
3227:
3214:
3213:
3209:
3201:
3197:
3189:
3185:
3167:
3166:
3162:
3155:
3140:
3139:
3135:
3122:. p. 127.
3111:
3110:
3106:
3097:
3095:
3091:
3060:
3052:
3051:
3047:
3040:
3027:
3026:
3022:
3007:
3006:
3002:
2997:
2992:
2978:Number sentence
2943:
2934:
2873:
2872:
2870:
2849:
2848:
2846:
2825:
2824:
2822:
2818:
2767:
2766:
2764:
2763:. For example,
2757:bivalent logics
2706:
2666:
2644:
2606:
2605:
2575:primitive types
2571:resulting value
2515:
2509:
2445:
2437:
2436:
2381:
2361:
2360:
2345:
2305:
2298:
2287:
2280:
2272:
2271:
2261:
2258:
2255:
2254:
2252:
2233:
2230:rational number
2188:
2183:
2152:lambda calculus
2125:
2123:Lambda calculus
2119:
2117:Lambda calculus
2093:
2083:
2082:
2052:
2051:
2028:
2027:
2008:
2007:
1988:
1987:
1941:
1934:
1933:
1914:
1913:
1894:
1893:
1872:
1859:
1854:
1853:
1848:can denote the
1830:
1829:
1798:
1776:
1763:
1752:
1751:
1725:
1703:
1690:
1685:
1684:
1681:n-ary operation
1661:
1660:
1636:
1635:
1616:
1615:
1577:
1573:
1513:
1512:
1478:formal language
1474:
1446:
1445:
1406:
1398:Main articles:
1396:
1345:
1344:
1315:
1309:
1304:
1298:
1257:
1216:
1215:
1208:
1144:
1143:
1136:
1130:
1124:
1069:
1068:
1044:
1043:
976:
955:
954:
940:
913:
912:
886:
818:
814:
798:
786:
775:
762:
737:
736:
675:
671:
661:
649:
643:
640:
639:
598:
597:
549:
547:
536:
529:
528:
477:
468:
467:
427:
426:
394:
393:
385:
310:
290:
289:
262:
251:
250:
221:
220:
219:and totally to
195:
194:
163:
162:
117:
116:
88:
87:
37:conventions of
17:
12:
11:
5:
5247:
5245:
5237:
5236:
5231:
5226:
5216:
5215:
5209:
5208:
5194:
5191:
5190:
5188:
5187:
5182:
5177:
5172:
5167:
5166:
5165:
5155:
5150:
5145:
5136:
5131:
5126:
5121:
5119:Abstract logic
5115:
5113:
5109:
5108:
5106:
5105:
5100:
5098:Turing machine
5095:
5090:
5085:
5080:
5075:
5070:
5069:
5068:
5063:
5058:
5053:
5048:
5038:
5036:Computable set
5033:
5028:
5023:
5018:
5012:
5010:
5004:
5003:
5001:
5000:
4995:
4990:
4985:
4980:
4975:
4970:
4965:
4964:
4963:
4958:
4953:
4943:
4938:
4933:
4931:Satisfiability
4928:
4923:
4918:
4917:
4916:
4906:
4905:
4904:
4894:
4893:
4892:
4887:
4882:
4877:
4872:
4862:
4861:
4860:
4855:
4848:Interpretation
4844:
4842:
4836:
4835:
4833:
4832:
4827:
4822:
4817:
4812:
4802:
4797:
4796:
4795:
4794:
4793:
4783:
4778:
4768:
4763:
4758:
4753:
4748:
4743:
4737:
4735:
4729:
4728:
4725:
4724:
4722:
4721:
4713:
4712:
4711:
4710:
4705:
4704:
4703:
4698:
4693:
4673:
4672:
4671:
4669:minimal axioms
4666:
4655:
4654:
4653:
4642:
4641:
4640:
4635:
4630:
4625:
4620:
4615:
4602:
4600:
4581:
4580:
4578:
4577:
4576:
4575:
4563:
4558:
4557:
4556:
4551:
4546:
4541:
4531:
4526:
4521:
4516:
4515:
4514:
4509:
4499:
4498:
4497:
4492:
4487:
4482:
4472:
4467:
4466:
4465:
4460:
4455:
4445:
4444:
4443:
4438:
4433:
4428:
4423:
4418:
4408:
4403:
4398:
4393:
4392:
4391:
4386:
4381:
4376:
4366:
4361:
4359:Formation rule
4356:
4351:
4350:
4349:
4344:
4334:
4333:
4332:
4322:
4317:
4312:
4307:
4301:
4295:
4278:Formal systems
4274:
4273:
4270:
4269:
4267:
4266:
4261:
4256:
4251:
4246:
4241:
4236:
4231:
4226:
4221:
4220:
4219:
4214:
4203:
4201:
4197:
4196:
4194:
4193:
4192:
4191:
4181:
4176:
4175:
4174:
4167:Large cardinal
4164:
4159:
4154:
4149:
4144:
4130:
4129:
4128:
4123:
4118:
4103:
4101:
4091:
4090:
4088:
4087:
4086:
4085:
4080:
4075:
4065:
4060:
4055:
4050:
4045:
4040:
4035:
4030:
4025:
4020:
4015:
4010:
4004:
4002:
3995:
3994:
3992:
3991:
3990:
3989:
3984:
3979:
3974:
3969:
3964:
3956:
3955:
3954:
3949:
3939:
3934:
3932:Extensionality
3929:
3927:Ordinal number
3924:
3914:
3909:
3908:
3907:
3896:
3890:
3884:
3883:
3880:
3879:
3877:
3876:
3871:
3866:
3861:
3856:
3851:
3846:
3845:
3844:
3834:
3833:
3832:
3819:
3817:
3811:
3810:
3808:
3807:
3806:
3805:
3800:
3795:
3785:
3780:
3775:
3770:
3765:
3760:
3754:
3752:
3746:
3745:
3743:
3742:
3737:
3732:
3727:
3722:
3717:
3712:
3711:
3710:
3700:
3695:
3690:
3685:
3680:
3675:
3669:
3667:
3658:
3652:
3651:
3649:
3648:
3643:
3638:
3633:
3628:
3623:
3611:Cantor's
3609:
3604:
3599:
3589:
3587:
3574:
3573:
3571:
3570:
3565:
3560:
3555:
3550:
3545:
3540:
3535:
3530:
3525:
3520:
3515:
3510:
3509:
3508:
3497:
3495:
3491:
3490:
3485:
3483:
3482:
3475:
3468:
3460:
3454:
3453:
3427:
3424:
3421:
3420:
3410:
3409:
3406:
3405:
3385:
3372:
3356:
3330:
3311:(2): 346â366.
3301:Church, Alonzo
3292:
3276:
3255:
3232:
3225:
3207:
3195:
3183:
3160:
3153:
3133:
3104:
3071:(6): 377â387.
3045:
3038:
3020:
2999:
2998:
2996:
2993:
2991:
2990:
2985:
2980:
2975:
2970:
2965:
2960:
2955:
2950:
2944:
2942:
2939:
2916:
2913:
2910:
2907:
2904:
2901:
2898:
2895:
2892:
2889:
2886:
2883:
2880:
2856:
2832:
2804:
2801:
2798:
2795:
2792:
2789:
2786:
2783:
2780:
2777:
2774:
2761:interpretation
2745:atomic formula
2705:
2702:
2628:
2625:
2622:
2619:
2616:
2613:
2591:floating-point
2511:Main article:
2508:
2505:
2493:canonical form
2478:
2475:
2472:
2469:
2466:
2463:
2460:
2457:
2452:
2448:
2444:
2425:distributivity
2402:
2399:
2396:
2393:
2388:
2384:
2380:
2377:
2374:
2371:
2368:
2357:indeterminates
2344:
2341:
2330:
2329:
2312:
2308:
2304:
2301:
2294:
2290:
2286:
2283:
2226:exponentiation
2218:multiplication
2187:
2184:
2182:
2179:
2144:Stephen Kleene
2121:Main article:
2118:
2115:
2099:
2096:
2092:
2070:
2067:
2064:
2037:
2015:
1995:
1976:
1975:
1964:
1948:
1944:
1921:
1901:
1879:
1875:
1871:
1866:
1862:
1837:
1822:
1821:is also a WFE.
1810:
1805:
1801:
1797:
1794:
1791:
1788:
1783:
1779:
1775:
1770:
1766:
1762:
1759:
1747:
1746:
1732:
1728:
1724:
1721:
1718:
1715:
1710:
1706:
1702:
1697:
1693:
1668:
1656:
1655:
1643:
1623:
1604:
1603:
1599:
1598:
1582:
1581:
1561:
1560:
1559:(T or F), etc.
1544:
1541:
1538:
1535:
1532:
1529:
1526:
1523:
1520:
1473:
1470:
1453:
1395:
1392:
1388:
1387:
1375:
1371:
1367:
1364:
1361:
1358:
1355:
1352:
1313:Syntax (logic)
1311:Main article:
1308:
1305:
1302:Formal grammar
1300:Main article:
1297:
1294:
1282:
1279:
1274:
1271:
1268:
1262:
1256:
1253:
1250:
1247:
1244:
1239:
1234:
1231:
1228:
1224:
1207:The value for
1196:
1193:
1190:
1187:
1184:
1181:
1178:
1175:
1172:
1167:
1162:
1159:
1156:
1152:
1112:
1109:
1106:
1103:
1100:
1097:
1092:
1087:
1084:
1081:
1077:
1054:
1051:
1035:
1034:
1023:
1012:
1009:
1004:
1001:
998:
994:
991:
988:
985:
980:
970:
966:
962:
928:
924:
920:
898:bound variable
885:
882:
881:
880:
879:
878:
867:
864:
861:
857:
854:
851:
848:
845:
842:
839:
831:
828:
825:
821:
817:
811:
808:
805:
801:
792:
789:
782:
778:
774:
771:
768:
765:
757:
752:
748:
744:
725:
722:
719:
716:
713:
710:
707:
702:
699:
696:
691:
682:
678:
674:
668:
664:
655:
652:
648:
642:
636:
631:
628:
625:
621:
617:
614:
611:
608:
605:
589:
588:
587:
586:
567:
564:
558:
553:
545:
542:
539:
523:
522:
521:
520:
504:
501:
498:
495:
492:
486:
481:
475:
462:
461:
460:
459:
443:
440:
437:
434:
421:
420:
419:
418:
407:
404:
401:
384:
381:
325:
322:
317:
313:
309:
306:
303:
300:
297:
277:
274:
269:
265:
261:
258:
228:
208:
205:
202:
182:
179:
176:
173:
170:
150:is a formula.
139:
136:
133:
130:
127:
124:
104:
101:
98:
95:
15:
13:
10:
9:
6:
4:
3:
2:
5246:
5235:
5232:
5230:
5227:
5225:
5222:
5221:
5219:
5206:
5205:
5200:
5192:
5186:
5183:
5181:
5178:
5176:
5173:
5171:
5168:
5164:
5161:
5160:
5159:
5156:
5154:
5151:
5149:
5146:
5144:
5140:
5137:
5135:
5132:
5130:
5127:
5125:
5122:
5120:
5117:
5116:
5114:
5110:
5104:
5101:
5099:
5096:
5094:
5093:Recursive set
5091:
5089:
5086:
5084:
5081:
5079:
5076:
5074:
5071:
5067:
5064:
5062:
5059:
5057:
5054:
5052:
5049:
5047:
5044:
5043:
5042:
5039:
5037:
5034:
5032:
5029:
5027:
5024:
5022:
5019:
5017:
5014:
5013:
5011:
5009:
5005:
4999:
4996:
4994:
4991:
4989:
4986:
4984:
4981:
4979:
4976:
4974:
4971:
4969:
4966:
4962:
4959:
4957:
4954:
4952:
4949:
4948:
4947:
4944:
4942:
4939:
4937:
4934:
4932:
4929:
4927:
4924:
4922:
4919:
4915:
4912:
4911:
4910:
4907:
4903:
4902:of arithmetic
4900:
4899:
4898:
4895:
4891:
4888:
4886:
4883:
4881:
4878:
4876:
4873:
4871:
4868:
4867:
4866:
4863:
4859:
4856:
4854:
4851:
4850:
4849:
4846:
4845:
4843:
4841:
4837:
4831:
4828:
4826:
4823:
4821:
4818:
4816:
4813:
4810:
4809:from ZFC
4806:
4803:
4801:
4798:
4792:
4789:
4788:
4787:
4784:
4782:
4779:
4777:
4774:
4773:
4772:
4769:
4767:
4764:
4762:
4759:
4757:
4754:
4752:
4749:
4747:
4744:
4742:
4739:
4738:
4736:
4734:
4730:
4720:
4719:
4715:
4714:
4709:
4708:non-Euclidean
4706:
4702:
4699:
4697:
4694:
4692:
4691:
4687:
4686:
4684:
4681:
4680:
4678:
4674:
4670:
4667:
4665:
4662:
4661:
4660:
4656:
4652:
4649:
4648:
4647:
4643:
4639:
4636:
4634:
4631:
4629:
4626:
4624:
4621:
4619:
4616:
4614:
4611:
4610:
4608:
4604:
4603:
4601:
4596:
4590:
4585:Example
4582:
4574:
4569:
4568:
4567:
4564:
4562:
4559:
4555:
4552:
4550:
4547:
4545:
4542:
4540:
4537:
4536:
4535:
4532:
4530:
4527:
4525:
4522:
4520:
4517:
4513:
4510:
4508:
4505:
4504:
4503:
4500:
4496:
4493:
4491:
4488:
4486:
4483:
4481:
4478:
4477:
4476:
4473:
4471:
4468:
4464:
4461:
4459:
4456:
4454:
4451:
4450:
4449:
4446:
4442:
4439:
4437:
4434:
4432:
4429:
4427:
4424:
4422:
4419:
4417:
4414:
4413:
4412:
4409:
4407:
4404:
4402:
4399:
4397:
4394:
4390:
4387:
4385:
4382:
4380:
4377:
4375:
4372:
4371:
4370:
4367:
4365:
4362:
4360:
4357:
4355:
4352:
4348:
4345:
4343:
4342:by definition
4340:
4339:
4338:
4335:
4331:
4328:
4327:
4326:
4323:
4321:
4318:
4316:
4313:
4311:
4308:
4306:
4303:
4302:
4299:
4296:
4294:
4290:
4285:
4279:
4275:
4265:
4262:
4260:
4257:
4255:
4252:
4250:
4247:
4245:
4242:
4240:
4237:
4235:
4232:
4230:
4229:KripkeâPlatek
4227:
4225:
4222:
4218:
4215:
4213:
4210:
4209:
4208:
4205:
4204:
4202:
4198:
4190:
4187:
4186:
4185:
4182:
4180:
4177:
4173:
4170:
4169:
4168:
4165:
4163:
4160:
4158:
4155:
4153:
4150:
4148:
4145:
4142:
4138:
4134:
4131:
4127:
4124:
4122:
4119:
4117:
4114:
4113:
4112:
4108:
4105:
4104:
4102:
4100:
4096:
4092:
4084:
4081:
4079:
4076:
4074:
4073:constructible
4071:
4070:
4069:
4066:
4064:
4061:
4059:
4056:
4054:
4051:
4049:
4046:
4044:
4041:
4039:
4036:
4034:
4031:
4029:
4026:
4024:
4021:
4019:
4016:
4014:
4011:
4009:
4006:
4005:
4003:
4001:
3996:
3988:
3985:
3983:
3980:
3978:
3975:
3973:
3970:
3968:
3965:
3963:
3960:
3959:
3957:
3953:
3950:
3948:
3945:
3944:
3943:
3940:
3938:
3935:
3933:
3930:
3928:
3925:
3923:
3919:
3915:
3913:
3910:
3906:
3903:
3902:
3901:
3898:
3897:
3894:
3891:
3889:
3885:
3875:
3872:
3870:
3867:
3865:
3862:
3860:
3857:
3855:
3852:
3850:
3847:
3843:
3840:
3839:
3838:
3835:
3831:
3826:
3825:
3824:
3821:
3820:
3818:
3816:
3812:
3804:
3801:
3799:
3796:
3794:
3791:
3790:
3789:
3786:
3784:
3781:
3779:
3776:
3774:
3771:
3769:
3766:
3764:
3761:
3759:
3756:
3755:
3753:
3751:
3750:Propositional
3747:
3741:
3738:
3736:
3733:
3731:
3728:
3726:
3723:
3721:
3718:
3716:
3713:
3709:
3706:
3705:
3704:
3701:
3699:
3696:
3694:
3691:
3689:
3686:
3684:
3681:
3679:
3678:Logical truth
3676:
3674:
3671:
3670:
3668:
3666:
3662:
3659:
3657:
3653:
3647:
3644:
3642:
3639:
3637:
3634:
3632:
3629:
3627:
3624:
3622:
3618:
3614:
3610:
3608:
3605:
3603:
3600:
3598:
3594:
3591:
3590:
3588:
3586:
3580:
3575:
3569:
3566:
3564:
3561:
3559:
3556:
3554:
3551:
3549:
3546:
3544:
3541:
3539:
3536:
3534:
3531:
3529:
3526:
3524:
3521:
3519:
3516:
3514:
3511:
3507:
3504:
3503:
3502:
3499:
3498:
3496:
3492:
3488:
3481:
3476:
3474:
3469:
3467:
3462:
3461:
3458:
3444:on 2014-11-15
3443:
3439:
3435:
3430:
3429:
3425:
3415:
3412:
3398:
3397:
3389:
3386:
3382:
3376:
3373:
3369:
3365:
3360:
3357:
3353:
3349:
3344:
3343:
3334:
3331:
3326:
3322:
3318:
3314:
3310:
3306:
3302:
3296:
3293:
3287:
3283:
3279:
3273:
3269:
3265:
3259:
3256:
3250:
3246:
3242:
3236:
3233:
3228:
3222:
3218:
3211:
3208:
3205:
3199:
3196:
3193:
3187:
3184:
3178:
3174:
3170:
3164:
3161:
3156:
3150:
3146:
3145:
3137:
3134:
3129:
3125:
3121:
3117:
3116:
3108:
3105:
3090:
3086:
3082:
3078:
3074:
3070:
3066:
3059:
3056:(June 1970).
3055:
3049:
3046:
3041:
3035:
3031:
3024:
3021:
3016:
3012:
3011:
3004:
3001:
2994:
2989:
2986:
2984:
2981:
2979:
2976:
2974:
2971:
2969:
2966:
2964:
2961:
2959:
2956:
2954:
2951:
2949:
2946:
2945:
2940:
2938:
2932:
2931:real-numbered
2914:
2911:
2905:
2902:
2899:
2893:
2887:
2884:
2881:
2854:
2830:
2799:
2796:
2793:
2787:
2781:
2778:
2775:
2762:
2758:
2754:
2750:
2746:
2742:
2738:
2734:
2730:
2725:
2723:
2719:
2715:
2711:
2703:
2701:
2700:
2695:
2693:
2688:
2684:
2680:
2672:
2663:
2659:
2657:
2652:
2650:
2642:
2626:
2623:
2620:
2617:
2614:
2611:
2603:
2598:
2596:
2592:
2588:
2584:
2580:
2576:
2572:
2568:
2564:
2560:
2556:
2552:
2548:
2544:
2540:
2536:
2532:
2528:
2524:
2520:
2514:
2506:
2504:
2502:
2501:expanded form
2498:
2494:
2489:
2476:
2473:
2470:
2467:
2464:
2461:
2458:
2455:
2450:
2446:
2442:
2434:
2430:
2426:
2422:
2421:commutativity
2418:
2417:associativity
2413:
2400:
2397:
2394:
2391:
2386:
2378:
2375:
2372:
2366:
2358:
2354:
2350:
2342:
2340:
2339:
2335:
2310:
2306:
2302:
2299:
2292:
2288:
2284:
2281:
2270:
2269:
2268:
2250:
2245:
2241:
2237:
2231:
2227:
2223:
2219:
2215:
2211:
2207:
2203:
2199:
2195:
2194:
2185:
2180:
2178:
2176:
2172:
2167:
2165:
2161:
2157:
2156:formal system
2153:
2149:
2145:
2141:
2140:Alonzo Church
2137:
2132:
2130:
2124:
2116:
2114:
2097:
2094:
2090:
2065:
2035:
2013:
1993:
1985:
1981:
1973:
1969:
1965:
1946:
1942:
1899:
1892:is a WFE. Or
1877:
1873:
1869:
1864:
1860:
1851:
1835:
1827:
1823:
1803:
1799:
1795:
1792:
1789:
1786:
1781:
1777:
1773:
1768:
1764:
1757:
1749:
1748:
1730:
1726:
1722:
1719:
1716:
1713:
1708:
1704:
1700:
1695:
1691:
1682:
1666:
1658:
1657:
1641:
1621:
1613:
1609:
1608:
1607:
1601:
1600:
1596:
1592:
1589:representing
1588:
1584:
1583:
1571:
1567:
1563:
1562:
1558:
1539:
1536:
1533:
1530:
1527:
1521:
1510:
1506:
1502:
1498:
1494:
1493:
1492:
1491:consists of:
1490:
1485:
1483:
1479:
1471:
1469:
1467:
1451:
1442:
1436:
1434:
1430:
1426:
1422:
1418:
1414:
1409:
1405:
1401:
1393:
1391:
1373:
1369:
1365:
1362:
1359:
1353:
1350:
1343:
1342:
1341:
1339:
1335:
1330:
1328:
1324:
1320:
1314:
1306:
1303:
1295:
1293:
1280:
1277:
1272:
1269:
1266:
1251:
1248:
1245:
1237:
1232:
1229:
1226:
1222:
1211:
1194:
1191:
1188:
1185:
1179:
1176:
1173:
1165:
1160:
1157:
1154:
1150:
1140:
1133:
1127:
1123:the variable
1110:
1104:
1101:
1098:
1090:
1085:
1082:
1079:
1075:
1065:
1052:
1049:
1041:
1032:
1028:
1024:
1010:
1007:
1002:
999:
996:
992:
989:
986:
983:
968:
964:
960:
953:
952:
951:
947:
943:
926:
922:
918:
909:
907:
901:
899:
895:
894:free variable
891:
883:
865:
862:
859:
849:
843:
837:
829:
826:
823:
819:
815:
809:
806:
803:
799:
790:
787:
780:
772:
769:
766:
755:
750:
746:
742:
717:
711:
705:
700:
697:
694:
689:
680:
676:
672:
666:
662:
653:
650:
646:
634:
629:
626:
623:
619:
615:
609:
603:
596:
595:
594:
593:
592:
584:
581: (
565:
562:
556:
551:
543:
540:
537:
527:
526:
525:
524:
518:
515: (
502:
499:
496:
493:
490:
484:
479:
473:
466:
465:
464:
463:
457:
454: (
441:
438:
435:
432:
425:
424:
423:
422:
405:
402:
399:
392:
391:
390:
389:
388:
382:
380:
378:
377:syntactically
374:
370:
366:
362:
359:is a kind of
358:
353:
351:
347:
343:
339:
323:
320:
315:
311:
307:
301:
295:
275:
272:
267:
263:
256:
248:
244:
239:
226:
206:
203:
200:
180:
177:
174:
171:
168:
160:
156:
151:
137:
134:
131:
128:
125:
122:
102:
99:
96:
93:
85:
81:
77:
73:
72:
66:
64:
60:
56:
52:
48:
44:
40:
36:
32:
28:
24:
19:
5195:
4993:Ultraproduct
4840:Model theory
4805:Independence
4741:Formal proof
4733:Proof theory
4716:
4689:
4646:real numbers
4618:second-order
4529:Substitution
4406:Metalanguage
4347:conservative
4324:
4320:Axiom schema
4264:Constructive
4234:MorseâKelley
4200:Set theories
4179:Aleph number
4172:inaccessible
4078:Grothendieck
3962:intersection
3849:Higher-order
3837:Second-order
3783:Truth tables
3740:Venn diagram
3523:Formal proof
3446:. Retrieved
3442:the original
3437:
3414:
3395:
3388:
3380:
3375:
3367:
3364:Mitchell, J.
3359:
3351:
3341:
3333:
3308:
3307:. Series 2.
3304:
3295:
3267:
3264:Hermes, Hans
3258:
3249:Model Theory
3248:
3235:
3216:
3210:
3198:
3186:
3177:Model Theory
3176:
3163:
3143:
3136:
3114:
3107:
3096:. Retrieved
3068:
3064:
3048:
3029:
3023:
3009:
3003:
2726:
2713:
2707:
2696:
2676:
2653:
2648:
2640:
2599:
2566:
2529:entity in a
2522:
2516:
2500:
2496:
2492:
2490:
2414:
2346:
2331:
2243:
2239:
2235:
2191:
2189:
2168:
2133:
2126:
1977:
1826:real numbers
1679:denote some
1605:
1602:Brackets ( )
1557:truth values
1486:
1484:as follows:
1475:
1437:
1424:
1410:
1407:
1389:
1337:
1331:
1316:
1209:
1138:
1131:
1125:
1066:
1036:
1030:
945:
941:
910:
902:
887:
590:
386:
372:
356:
354:
345:
240:
158:
154:
152:
69:
67:
26:
20:
18:
5103:Type theory
5051:undecidable
4983:Truth value
4870:equivalence
4549:non-logical
4162:Enumeration
4152:Isomorphism
4099:cardinality
4083:Von Neumann
4048:Ultrafilter
4013:Uncountable
3947:equivalence
3864:Quantifiers
3854:Fixed-point
3823:First-order
3703:Consistency
3688:Proposition
3665:Traditional
3636:Lindström's
3626:Compactness
3568:Type theory
3513:Cardinality
2759:, given an
2729:first-order
2677:Except for
2651:otherwise.
2559:association
2497:normal form
2249:square root
2214:subtraction
2171:undecidable
2129:formalizing
1980:syntax tree
1972:associative
1963:is as well.
1319:well-formed
80:noun phrase
59:punctuation
23:mathematics
5218:Categories
4914:elementary
4607:arithmetic
4475:Quantifier
4453:functional
4325:Expression
4043:Transitive
3987:identities
3972:complement
3905:hereditary
3888:Set theory
3448:2012-03-18
3426:References
3277:3540058192
3241:C.C. Chang
3169:C.C. Chang
3118:. Boston:
3098:2020-04-29
2958:Combinator
2656:statements
2577:, such as
2567:evaluation
2523:expression
2429:polynomial
2332:See also:
2204:, and the
1984:leaf nodes
1591:operations
1568:amount of
1503:, such as
1466:direct sum
1334:arithmetic
1142:; that is
346:equivalent
61:signs and
51:operations
27:expression
5185:Supertask
5088:Recursion
5046:decidable
4880:saturated
4858:of models
4781:deductive
4776:axiomatic
4696:Hilbert's
4683:Euclidean
4664:canonical
4587:axiomatic
4519:Signature
4448:Predicate
4337:Extension
4259:Ackermann
4184:Operation
4063:Universal
4053:Recursive
4028:Singleton
4023:Inhabited
4008:Countable
3998:Types of
3982:power set
3952:partition
3869:Predicate
3815:Predicate
3730:Syllogism
3720:Soundness
3693:Inference
3683:Tautology
3585:paradoxes
3286:1431-4657
3085:207549016
2973:Rewriting
2933:value of
2912:≥
2894:∗
2855:∗
2788:∗
2683:variables
2624:≥
2618:−
2551:operators
2547:functions
2543:variables
2539:constants
2527:syntactic
2456:−
2392:−
2285:−
2202:variables
2148:functions
2014:∪
1943:ϕ
1920:√
1874:ϕ
1861:ϕ
1800:ϕ
1778:ϕ
1765:ϕ
1727:ϕ
1705:ϕ
1692:ϕ
1570:variables
1519:∅
1452:⊕
1425:1 + 2 Ă 3
1421:semantics
1417:variables
1400:Semantics
1394:Semantics
1351:×
1338:1 + 2 Ă 3
1323:operators
1223:∑
1186:≡
1151:∑
1076:∑
1050:≡
1027:undefined
906:operation
890:variables
770:−
747:∫
620:∑
541:−
500:−
439:−
260:↦
247:arguments
204:−
178:−
172:×
155:evaluated
135:≥
129:−
100:−
55:functions
47:variables
43:constants
35:syntactic
5170:Logicism
5163:timeline
5139:Concrete
4998:Validity
4968:T-schema
4961:Kripke's
4956:Tarski's
4951:semantic
4941:Strength
4890:submodel
4885:spectrum
4853:function
4701:Tarski's
4690:Elements
4677:geometry
4633:Robinson
4554:variable
4539:function
4512:spectrum
4502:Sentence
4458:variable
4401:Language
4354:Relation
4315:Automata
4305:Alphabet
4289:language
4143:-jection
4121:codomain
4107:Function
4068:Universe
4038:Infinite
3942:Relation
3725:Validity
3715:Argument
3613:theorem,
3383:, p. 120
3266:(1973).
3247:(1977).
3175:(1977).
3128:68015225
3089:Archived
2941:See also
2731:term is
2722:formulas
2687:sequence
2563:stateful
2222:division
2210:addition
2162:and the
2158:used in
1852:+, then
1555:, ...),
1489:alphabet
1441:equation
1390:is not.
1040:identity
383:Examples
350:semantic
243:function
84:sentence
63:brackets
5112:Related
4909:Diagram
4807: (
4786:Hilbert
4771:Systems
4766:Theorem
4644:of the
4589:systems
4369:Formula
4364:Grammar
4280: (
4224:General
3937:Forcing
3922:Element
3842:Monadic
3617:paradox
3558:Theorem
3494:General
3370:, p. 26
3325:1968337
2927:
2871:
2867:
2847:
2843:
2823:
2815:
2765:
2679:numbers
2595:complex
2587:integer
2583:Boolean
2557:and of
2353:scalars
2265:
2253:
1932:, then
1505:numbers
1499:in the
1497:objects
1413:algebra
71:formula
31:symbols
4875:finite
4638:Skolem
4591:
4566:Theory
4534:Symbol
4524:String
4507:atomic
4384:ground
4379:closed
4374:atomic
4330:ground
4293:syntax
4189:binary
4116:domain
4033:Finite
3798:finite
3656:Logics
3615:
3563:Theory
3323:
3284:
3274:
3223:
3151:
3126:
3083:
3036:
2692:matrix
2579:string
2549:, and
2415:Using
1982:. The
1634:" or "
1480:, and
1307:Syntax
973:
944:= 10,
365:symols
361:string
338:square
53:, and
4865:Model
4613:Peano
4470:Proof
4310:Arity
4239:Naive
4126:image
4058:Fuzzy
4018:Empty
3967:union
3912:Class
3553:Model
3543:Lemma
3501:Axiom
3400:(PDF)
3321:JSTOR
3092:(PDF)
3081:S2CID
3061:(PDF)
2995:Notes
2753:false
2718:terms
2697:See:
2669:as a
2641:false
2593:, or
2535:value
2525:is a
2521:, an
2499:, or
2228:by a
1750:Then
1576:, or
896:or a
25:, an
4988:Type
4791:list
4595:list
4572:list
4561:Term
4495:rank
4389:open
4283:list
4095:Maps
4000:sets
3859:Free
3829:list
3579:list
3506:list
3282:ISSN
3272:ISBN
3221:ISBN
3149:ISBN
3124:LCCN
3034:ISBN
2845:and
2749:true
2712:, a
2681:and
2671:Lisp
2649:true
2423:and
2336:and
2224:and
2154:, a
2142:and
2081:and
2006:and
1659:Let
1509:sets
1487:The
1402:and
1029:for
288:and
4675:of
4657:of
4605:of
4137:Sur
4111:Map
3918:Ur-
3900:Set
3313:doi
3073:doi
2755:in
2751:or
2720:or
2708:In
2643:if
2600:In
2597:).
2517:In
2238:â 2
2190:An
1435:).
1411:In
1281:36.
1212:= 3
1137:12
1033:= 0
948:= 5
363:of
227:11.
157:or
45:),
21:In
5220::
5061:NP
4685::
4679::
4609::
4286:),
4141:Bi
4133:In
3436:.
3350:.
3348:74
3319:.
3309:33
3280:.
3243:;
3171:;
3087:.
3079:.
3069:13
3067:.
3063:.
3013:.
2937:.
2727:A
2589:,
2581:,
2545:,
2541:,
2495:,
2477:3.
2419:,
2347:A
2242:+
2240:xy
2220:,
2216:,
2212:,
2200:,
2177:)
2166:.
2059:ln
2050:,
1828:,
1468:.
1189:12
1011:2.
990:10
900:.
566:12
503:10
355:A
201:16
49:,
5141:/
5056:P
4811:)
4597:)
4593:(
4490:â
4485:!
4480:â
4441:=
4436:â
4431:â
4426:â§
4421:âš
4416:ÂŹ
4139:/
4135:/
4109:/
3920:)
3916:(
3803:â
3793:3
3581:)
3479:e
3472:t
3465:v
3451:.
3327:.
3315::
3288:.
3229:.
3157:.
3130:.
3101:.
3075::
3042:.
3017:.
2935:x
2915:0
2909:)
2906:1
2903:+
2900:x
2897:(
2891:)
2888:1
2885:+
2882:x
2879:(
2831:+
2819:x
2803:)
2800:1
2797:+
2794:x
2791:(
2785:)
2782:1
2779:+
2776:x
2773:(
2645:x
2627:3
2621:5
2615:x
2612:8
2474:+
2471:x
2468:6
2465:+
2462:y
2459:x
2451:2
2447:x
2443:3
2401:.
2398:y
2395:x
2387:2
2383:)
2379:1
2376:+
2373:x
2370:(
2367:3
2311:2
2307:x
2303:+
2300:1
2293:2
2289:x
2282:1
2262:2
2259:/
2256:1
2244:c
2236:x
2234:3
2208:(
2098:x
2095:d
2091:d
2069:)
2066:x
2063:(
2036:x
1994:+
1974:)
1947:1
1900:F
1878:2
1870:+
1865:1
1836:F
1809:)
1804:n
1796:.
1793:.
1790:.
1787:,
1782:2
1774:,
1769:1
1761:(
1758:F
1731:n
1723:.
1720:.
1717:.
1714:,
1709:2
1701:,
1696:1
1667:F
1642:x
1622:2
1597:)
1580:)
1578:y
1574:x
1543:}
1540:3
1537:,
1534:2
1531:,
1528:1
1525:{
1522:,
1511:(
1386:.
1374:y
1370:/
1366:,
1363:+
1360:x
1357:)
1354:4
1278:=
1273:3
1270:=
1267:x
1261:|
1255:)
1252:x
1249:n
1246:2
1243:(
1238:3
1233:1
1230:=
1227:n
1210:x
1195:.
1192:x
1183:)
1180:x
1177:n
1174:2
1171:(
1166:3
1161:1
1158:=
1155:n
1139:x
1132:x
1126:n
1111:,
1108:)
1105:x
1102:n
1099:2
1096:(
1091:3
1086:1
1083:=
1080:n
1053:.
1031:y
1008:=
1003:5
1000:=
997:y
993:,
987:=
984:x
979:|
969:y
965:/
961:x
946:y
942:x
927:y
923:/
919:x
866:.
863:t
860:d
856:)
853:)
850:t
847:(
844:u
841:(
838:f
830:1
827:+
824:n
820:t
816:d
810:1
807:+
804:n
800:d
791:!
788:n
781:n
777:)
773:t
767:1
764:(
756:1
751:0
743:+
724:)
721:)
718:t
715:(
712:u
709:(
706:f
701:0
698:=
695:t
690:|
681:k
677:t
673:d
667:k
663:d
654:!
651:k
647:1
635:n
630:1
627:=
624:k
616:+
613:)
610:a
607:(
604:f
585:)
563:+
557:2
552:x
544:1
538:x
519:)
497:x
494:4
491:+
485:2
480:x
474:7
458:)
442:5
436:x
433:8
406:8
403:+
400:3
324:1
321:+
316:2
312:x
308:=
305:)
302:x
299:(
296:f
276:1
273:+
268:2
264:x
257:x
207:5
181:5
175:2
169:8
138:3
132:5
126:x
123:8
103:5
97:x
94:8
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.