The Arithmetic System

Arithmetic must be done in the context of the THF or TFF types logics, which support the predefined atomic numeric types $int, $rat, and $real. Using THF or TFF enforces semantics that separate $int from $rat from $real from $i from $o. The numbers are unbounded, and the reals of infinite precision (rather than some specific implementation such as 32 bit 2's complement integer, or IEEE floating point). Systems that implement limited arithmetic must halt in an SZS error state if they hit overflow.

The following interpreted predicates and interpreted functions are defined. The symbols are overloaded (i.e., ad-hoc polymorphic) for the provided type signatures.

Symbol Types Operation Comments, examples                                        -
$int $tType The type of integers 123, -123

<integer> ::- (<signed_integer>|<unsigned_integer>) <signed_integer> ::- <sign><unsigned_integer> <unsigned_integer> ::- <decimal> <decimal> ::- (<zero_numeric>|<positive_decimal>) <positive_decimal> ::- <non_zero_numeric><numeric>* <sign> ::: [+-] <zero_numeric> ::: [0] <non_zero_numeric> ::: [1-9] <numeric> ::: [0-9]

$rat $tType The type of rationals 123/456, -123/456, +123/456
<rational> ::- (<signed_rational>|<unsigned_rational>) <signed_rational> ::- <sign><unsigned_rational> <unsigned_rational> ::- <decimal><slash><positive_decimal> <slash> ::: [/]

$real $tType The type of reals 123.456, -123.456,
123.456E789, 123.456e789, -123.456E789,
123.456E-789, -123.456E-789
<real> ::- (<signed_real>|<unsigned_real>) <signed_real> ::- <sign><unsigned_real> <unsigned_real> ::- (<decimal_fraction>|<decimal_exponent>) <decimal_exponent> ::- (<decimal>|<decimal_fraction>)<exponent><decimal> <decimal_fraction> ::- <decimal><dot_decimal> <dot_decimal> ::- <dot><numeric><numeric>* <dot> ::: [.] <exponent> ::: [Ee]

= (infix) ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
Comparison of two numbers. The numbers must be the same atomic type (see the type system).
$less/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
Less-than comparison of two numbers. $less, $lesseq, $greater, and $greatereq are related by
  ! [X,Y] : ( $lesseq(X,Y) <=> ( $less(X,Y) | X = Y ) )
  ! [X,Y] : ( $greater(X,Y) <=> $less(Y,X) )
  ! [X,Y] : ( $greatereq(X,Y) <=> $lesseq(Y,X) )
i.e, only $less and equality need to be implemented to get all four relational operators.
$lesseq/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
Less-than-or-equal-to comparison of two numbers.
$greater/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
Greater-than comparison of two numbers.
$greatereq/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
Greater-than-or-equal-to comparison of two numbers.
$uminus/1 $int > $int
$rat > $rat
$real > $real
Unary minus of a number. $uminus, $sum, and $difference are related by
  ! [X,Y] : $difference(X,Y) = $sum(X,$uminus(Y))
i.e, only $uminus and $sum need to be implemented to get all three additive operators.
$sum/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
Sum of two numbers.
$difference/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
Difference between two numbers.
$product/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
Product of two numbers.
$quotient/2 ($int * $int) > $rat
($rat * $rat) > $rat
($real * $real) > $real
Exact quotient of two numbers of the same type. For non-zero divisors, the result can be computed. For zero divisors the result is not specified. In practice, if an ATP system does not "know" that the divisor is non-zero, it should simply not evaluate the $quotient. Users should always guard their use of $quotient using inequality, e.g.,
  ! [X: $real] : ( X != 0.0 => p($quotient(5.0,X)) )
For $rat or $real operands the result is the same type. For $int operands the result is $rat; the result might be simplied.
$quotient_e/2, $quotient_t/2, $quotient_f/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
Integral quotient of two numbers. The three variants use different rounding to an integral result:

$quotient_e(N,D) - the Euclidean quotient, which has a non-negative remainder. If D is positive then $quotient_e(N,D) is the floor (in the type of N and D) of the real division N/D, and if D is negative then $quotient_e(N,D) is the ceiling of N/D.
$quotient_t(N,D) - the truncation of the real division N/D.
$quotient_f(N,D) - the floor of the real division N/D.
For zero divisors the result is not specified.
$remainder_e/2, $remainder_t/2, $remainder_f/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
Remainder after integral division of two numbers. For τ ∈ {$int,$rat, $real}, ρ ∈ {e, t,f}, $quotient_ρ and $remainder_ρ are related by
  ! [N:τ,D:τ] : $sum($product($quotient_ρ(N,D),D),$remainder_ρ(N,D)) = N
For zero divisors the result is not specified.
$floor/1 $int > $int
$rat > $rat
$real > $real
Floor of a number. The largest integral value (in the type of the argument) not greater than the argument (i.e., ! [X] : ($is_int($floor(X)))).
$ceiling/1 $int > $int
$rat > $rat
$real > $real
Ceiling of a number. The smallest integral value (in the type of the argument) not less than the argument (i.e., ! [X] : ($is_int($ceiling(X)))).
$truncate/1 $int > $int
$rat > $rat
$real > $real
Truncation of a number. The nearest integral value (in the type of the argument) with magnitude not greater than the absolute value of the argument (i.e., ! [X] : ($is_int($truncate(X)))).
$round/1 $int > $int
$rat > $rat
$real > $real
Rounding of a number. The nearest integral value (in the type of the argument) to the argument (i.e., ! [X] : ($is_int($rount(X)))). If the argument is halfway between two integral values, the nearest even integral value to the argument.
$abs/1 $int > $int
$rat > $rat
$real > $real
Absolute value of a number. $abs is related to other operators by
! [X] : ( ( $greatereq(X,0) => $abs(X) = X ) & ( $less(X,0) => $abs(X) = $uminus(X) ) )

$is_int/1 $int > $o
$rat > $o
$real > $o
Test for coincidence with an $int value.
$is_rat/1 $int > $o
$rat > $o
$real > $o
Test for coincidence with a $rat value.
$to_int/1 $int > $int
$rat > $int
$real > $int
Coercion of a number to $int. The largest $int not greater than the argument; the argument effectively gets truncated before conversion: ! [X] : ($to_int($truncate(X)) = $to_int(X)). If applied to an argument of type $int, this is the identity function.
$to_rat/1 $int > $rat
$rat > $rat
$real > $rat
Coercion of a number to $rat. This function is not fully specified. If applied to an argument of type $int, the result is the argument over 1. If applied to an argument of type $rat, this is the identity function. If applied to an argument of type $real that is (known to be) rational, the result is the $rat value. For other reals the result is not specified. In practice, if an ATP system does not "know" that the argument is rational, it should simply not evaluate the $to_rat. Users should always guard their use of $to_rat using $is_rat, e.g.,
  ! [X: $real] : ( $is_rat(X) => p($to_rat(X)) )
$to_real/1 $int > $real
$rat > $real
$real > $real
Coercion of a number to $real. If applied to an argument of type $real, this is the identity function.

Symbol	Types	Operation	Comments, examples -
`$int`	`$tType`	The type of integers	`123`, `-123` <integer> ::- (<signed_integer>\|<unsigned_integer>) <signed_integer> ::- <sign><unsigned_integer> <unsigned_integer> ::- <decimal> <decimal> ::- (<zero_numeric>\|<positive_decimal>) <positive_decimal> ::- <non_zero_numeric><numeric>* <sign> ::: [+-] <zero_numeric> ::: [0] <non_zero_numeric> ::: [1-9] <numeric> ::: [0-9]
`$rat`	`$tType`	The type of rationals	`123/456`, `-123/456`, `+123/456` <rational> ::- (<signed_rational>\|<unsigned_rational>) <signed_rational> ::- <sign><unsigned_rational> <unsigned_rational> ::- <decimal><slash><positive_decimal> <slash> ::: [/]
`$real`	`$tType`	The type of reals	`123.456`, `-123.456`, `123.456E789`, `123.456e789`, `-123.456E789`, `123.456E-789`, `-123.456E-789` <real> ::- (<signed_real>\|<unsigned_real>) <signed_real> ::- <sign><unsigned_real> <unsigned_real> ::- (<decimal_fraction>\|<decimal_exponent>) <decimal_exponent> ::- (<decimal>\|<decimal_fraction>)<exponent><decimal> <decimal_fraction> ::- <decimal><dot_decimal> <dot_decimal> ::- <dot><numeric><numeric>* <dot> ::: [.] <exponent> ::: [Ee]
`=` (infix)	`($int * $int) > $o` `($rat * $rat) > $o` `($real * $real) > $o`	Comparison of two numbers.	The numbers must be the same atomic type (see the type system).
`$less`/2	`($int * $int) > $o` `($rat * $rat) > $o` `($real * $real) > $o`	Less-than comparison of two numbers.	`$less`, `$lesseq`, `$greater`, and `$greatereq` are related by `! [X,Y] : ( $lesseq(X,Y) <=> ( $less(X,Y) \| X = Y ) )` `! [X,Y] : ( $greater(X,Y) <=> $less(Y,X) )` `! [X,Y] : ( $greatereq(X,Y) <=> $lesseq(Y,X) )` i.e, only `$less` and equality need to be implemented to get all four relational operators.
`$lesseq`/2	`($int * $int) > $o` `($rat * $rat) > $o` `($real * $real) > $o`	Less-than-or-equal-to comparison of two numbers.
`$greater`/2	`($int * $int) > $o` `($rat * $rat) > $o` `($real * $real) > $o`	Greater-than comparison of two numbers.
`$greatereq`/2	`($int * $int) > $o` `($rat * $rat) > $o` `($real * $real) > $o`	Greater-than-or-equal-to comparison of two numbers.
`$uminus`/1	`$int > $int` `$rat > $rat` `$real > $real`	Unary minus of a number.	$uminus, `$sum`, and `$difference` are related by `! [X,Y] : $difference(X,Y) = $sum(X,$uminus(Y))` i.e, only `$uminus` and `$sum` need to be implemented to get all three additive operators.
`$sum`/2	`($int * $int) > $int` `($rat * $rat) > $rat` `($real * $real) > $real`	Sum of two numbers.
`$difference`/2	`($int * $int) > $int` `($rat * $rat) > $rat` `($real * $real) > $real`	Difference between two numbers.
`$product`/2	`($int * $int) > $int` `($rat * $rat) > $rat` `($real * $real) > $real`	Product of two numbers.
`$quotient`/2	`($int * $int) > $rat` `($rat * $rat) > $rat` `($real * $real) > $real`	Exact quotient of two numbers of the same type.	For non-zero divisors, the result can be computed. For zero divisors the result is not specified. In practice, if an ATP system does not "know" that the divisor is non-zero, it should simply not evaluate the `$quotient`. Users should always guard their use of `$quotient` using inequality, e.g., `! [X: $real] : ( X != 0.0 => p($quotient(5.0,X)) )` For `$rat` or `$real` operands the result is the same type. For `$int` operands the result is `$rat`; the result might be simplied.
`$quotient_e`/2, `$quotient_t`/2, `$quotient_f`/2	`($int * $int) > $int` `($rat * $rat) > $rat` `($real * $real) > $real`	Integral quotient of two numbers.	The three variants use different rounding to an integral result: `$quotient_e(N,D)` - the Euclidean quotient, which has a non-negative remainder. If `D` is positive then `$quotient_e(N,D)` is the floor (in the type of `N` and `D`) of the real division `N/D`, and if `D` is negative then `$quotient_e(N,D)` is the ceiling of `N/D`. `$quotient_t(N,D)` - the truncation of the real division `N/D`. `$quotient_f(N,D)` - the floor of the real division `N/D`. For zero divisors the result is not specified.
`$remainder_e`/2, `$remainder_t`/2, `$remainder_f`/2	`($int * $int) > $int` `($rat * $rat) > $rat` `($real * $real) > $real`	Remainder after integral division of two numbers.	For `τ` ∈ {`$int`,`$rat`, `$real`}, `ρ` ∈ {`e`, `t`,`f`}, `$quotient_ρ` and `$remainder_ρ` are related by `! [N:τ,D:τ] : $sum($product($quotient_ρ(N,D),D),$remainder_ρ(N,D)) = N` For zero divisors the result is not specified.
`$floor`/1	`$int > $int` `$rat > $rat` `$real > $real`	Floor of a number.	The largest integral value (in the type of the argument) not greater than the argument (i.e., `! [X] : ($is_int($floor(X)))`).
`$ceiling`/1	`$int > $int` `$rat > $rat` `$real > $real`	Ceiling of a number.	The smallest integral value (in the type of the argument) not less than the argument (i.e., `! [X] : ($is_int($ceiling(X)))`).
`$truncate`/1	`$int > $int` `$rat > $rat` `$real > $real`	Truncation of a number.	The nearest integral value (in the type of the argument) with magnitude not greater than the absolute value of the argument (i.e., `! [X] : ($is_int($truncate(X)))`).
`$round`/1	`$int > $int` `$rat > $rat` `$real > $real`	Rounding of a number.	The nearest integral value (in the type of the argument) to the argument (i.e., `! [X] : ($is_int($rount(X)))`). If the argument is halfway between two integral values, the nearest even integral value to the argument.
`$abs`/1	`$int > $int` `$rat > $rat` `$real > $real`	Absolute value of a number.	`$abs` is related to other operators by ! [X] : ( ( $greatereq(X,0) => $abs(X) = X ) & ( $less(X,0) => $abs(X) = $uminus(X) ) )
`$is_int`/1	`$int > $o` `$rat > $o` `$real > $o`	Test for coincidence with an `$int` value.
`$is_rat`/1	`$int > $o` `$rat > $o` `$real > $o`	Test for coincidence with a `$rat` value.
`$to_int`/1	`$int > $int` `$rat > $int` `$real > $int`	Coercion of a number to `$int`.	The largest `$int` not greater than the argument; the argument effectively gets truncated before conversion: `! [X] : ($to_int($truncate(X)) = $to_int(X))`. If applied to an argument of type `$int`, this is the identity function.
`$to_rat`/1	`$int > $rat` `$rat > $rat` `$real > $rat`	Coercion of a number to `$rat`.	This function is not fully specified. If applied to an argument of type `$int`, the result is the argument over `1`. If applied to an argument of type `$rat`, this is the identity function. If applied to an argument of type `$real` that is (known to be) rational, the result is the `$rat` value. For other reals the result is not specified. In practice, if an ATP system does not "know" that the argument is rational, it should simply not evaluate the `$to_rat`. Users should always guard their use of `$to_rat` using `$is_rat`, e.g., `! [X: $real] : ( $is_rat(X) => p($to_rat(X)) )`
`$to_real`/1	`$int > $real` `$rat > $real` `$real > $real`	Coercion of a number to `$real`.	If applied to an argument of type `$real`, this is the identity function.

The extent to which ATP systems are able to work with the arithmetic predicates and functions can vary, from a simple ability to evaluate ground terms, e.g., $sum(2,3) can be evaluated to 5, through an ability to instantiate variables in equations involving such functions, e.g., $product(2,$uminus(X)) = $uminus($sum(X,2)) can instantiate X to 2, to extensive algebraic manipulation capability. The syntax does not axiomatize arithmetic theory, but may be used to write axioms of the theory.