Wikipedia has related information atFirst-order logic.

We only give a very rough summary of FO here. An introduction can be found at FO.

Syntax is 'just' about sequences of signs.Thealphabet of FO consists of:

• Variables${\displaystyle x_0,x_1,x_2,...}$
• Logical Connectives:${\displaystyle \mathrm{\neg }}$,${\displaystyle \wedge }$
• Quantifiers:${\displaystyle \mathrm{\exists }}$
• Equality:${\displaystyle \equiv }$
• Parenthesis: ), (
• n-ary Relation symbols, for no or many n>0, e.g. R(., .)
• Constant symbols (none or many)

The handling of parenthesis is done the 'usual' way and is not formally described further.

For a given set of symbols S, variables and constant symbols are said to be S-Terms.

S-Expressions are obtained by the multiple application of the following rules:

• ${\displaystyle t_1\equiv t_2}$ is an expression
• ${\displaystyle R{t}_1...t_n}$ is an expression, for an n-ary relation symbol R
• ${\displaystyle \mathrm{\neg }\phi ,{\phi }_1\wedge {\phi }_2}$ are expressions
• ${\displaystyle {\mathrm{\exists }}_x\phi }$ is an expression

where${\displaystyle t_{.}}$ is a term and${\displaystyle {\phi }_{.}}$ an expression.

So additional connectives for OR, IMPLICATION, EQUIVALENCE etc. can be defined as well as the FOR ALL quantifier.

Semantics adds the meaning to the language in three steps:

• 1st it defines what the logical symbols (connectives and quantifiers) mean (this always holds in FO),
• 2nd it maps relation symbols and constant symbols to actual relations and constants over a given set of entities (this is usually defined per subject, like Analysis or Statistics) and
• 3rd it maps free variables (not bound to a quantifier) to entities (usually done per Problem, like solving an equation).

1st we assume theLogical Symbols${\displaystyle \mathrm{\neg },\wedge ,...,\mathrm{\exists }}$ to have the usual meaning.

2nd a S-Structure is a pair (A,a) of

• a nonempty setA, the Universe, and
• a mappinga from S, such that
  • each n-ary relation symbol is mapped to a n-ary relation onA and
  • each constant symbol is mapped to an element ofA

3rd an Interpretation is a pair${\displaystyle (\mathfrak{A},\beta )}$ where${\displaystyle \mathfrak{A}}$ = (A,a) is a S-Structure and${\displaystyle \beta }$ is a mapping from all free variables to an element ofA.

An Interpretation is said to be aModel of a set${\displaystyle \mathrm{\Phi }}$ of S-expressions (${\displaystyle \mathfrak{I}\models \mathrm{\Phi }}$) iff all of the following hold

• ${\displaystyle \mathfrak{I}(t_1)=\mathfrak{I}(t_1)}$, for${\displaystyle \mathfrak{I}\models t_1\equiv t_2}$
• ${\displaystyle R^n\mathfrak{I}(t_1),...,\mathfrak{I}(t_n)}$ , for${\displaystyle \mathfrak{I}\models R{t}_1...t_n}$
• Not${\displaystyle \mathfrak{I}\models \phi }$ , for${\displaystyle \mathfrak{I}\models \mathrm{\neg }\phi }$
• ${\displaystyle \mathfrak{I}\models {\phi }_0)}$ and${\displaystyle \mathfrak{I}\models {\phi }_1)}$, for${\displaystyle \mathfrak{I}\models {\phi }_0\wedge {\phi }_1}$
• It exists an${\displaystyle a\in A}$ s.t.${\displaystyle \mathfrak{I}\models \phi (a)}$, for${\displaystyle \mathfrak{I}\models {\mathrm{\exists }}_x\phi (x)}$

Wikipedia has related information atgame theory.

A game is described by

• its players (>1),
• its rules i.e.who playswhen andwhat is allowed to do and
• its possible ends and payoffs.

More formal, it's a tuple (P, T, m, u) where

• P (the Players) is a set, with |P| = n > 1
• is a graph on a set of nodes that forms a taxonomy, i.e. a T is a tree with a dedicated root node. The leafs called terminal nodes T all others decision nodes D. This describes the possible move sequences.
• m is a mapping from D to P, that says who is to move at what point.
• u is a set of mappings u_i (one for each player i) from T to an ordered set U, that give the payoff for a player at each terminal node.

We assume here and in the following that every player has perfect information (so the above definition is incomplete), i.e. all moves of all players made so far, and we don't consider move by chance. Common knowledge about the rules and players is assumed anyway. The above is called the extensive form representation of a game. Others like the normal form reptresentation make simplifying assumptions on this (e.g. about the information) and use the concept of strategy instead of single moves.

Notice that different moves can lead to the same 'position', i.e. a position can be represented more than once in a game-tree. And, the same payoffs can have different meanings to different players.

Counting a set can get messy due to

• counting things in an other than the natural order
• counting elements multiple times

...

Fix enumerations (without repetition) of the underlying sets:

Now we construct a one-to-one correspondence betweenA andB that is strictly increasing. Initially no member ofA is paired with any member ofB.

(1) Leti be the smallest index such thata_i is not yet paired with any member ofB. Letj be the smallest index such thatb_j is not yet paired with any member ofAanda_i can be paired withb_j consistently with the requirement that the pairing be strictly increasing. Paira_i withb_j.

(2) Letj be the smallest index such thatb_j is not yet paired with any member ofA. Leti be the smallest index such thata_i is not yet paired with any member ofBandb_j can be paired witha_i consistently with the requirement that the pairing be strictly increasing. Pairb_j witha_i.

(3) Go back to step(1).

It still has to be checked that the choice required in step(1) and(2) can actually be made in accordance to the requirements. Using step(1) as an example:

If there are alreadya_p anda_q inA corresponding tob_p andb_q inB respectively such that and, we chooseb_j in betweenb_p andb_q usingdensity. Otherwise, we choose a suitable large or small element ofB using the fact thatB hasneither a maximum nor a minimum. Choices made in step(2) are dually possible. Finally, the construction ends after countably many steps becauseA andBare countably infinite. Note that we had to use all the prerequisites.

If we iterated only step(1), rather than going back and forth, then the resulting pairing would fail to be bijective.

• Book:Finite Model Theory