Common expressions for the theory of proveit.logic.booleans.quantification¶
In [1]:
import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import k, A, B
from proveit.core_expr_types import (
x_1_to_n, x_1_to_m, y_1_to_n, y_1_to_m, z_1_to_n,
P__x_1_to_n, P__y_1_to_n, P__x_1_to_m_y_1_to_n,
Q__x_1_to_n, Q__x_1_to_m, Q__y_1_to_n, Q__z_1_to_n, R__x_1_to_n,
R__y_1_to_m, R__z_1_to_n, R__x_1_to_m_y_1_to_n)
from proveit.logic import TRUE, Implies, Not, Forall, Exists, NotExists, NotEquals
from proveit.numbers import Natural, NaturalPos
%begin common
In [2]:
general_forall_Px = Forall(x_1_to_n, P__x_1_to_n)
general_forall_Px: 
In [3]:
general_forall_Py= Forall(y_1_to_n, P__y_1_to_n)
general_forall_Py: 
In [4]:
general_forall_Px_if_Qx = Forall(x_1_to_n, P__x_1_to_n, conditions=[Q__x_1_to_n])
general_forall_Px_if_Qx: 
In [5]:
general_forall_Py_if_Qy = Forall(y_1_to_n, P__y_1_to_n, conditions=[Q__y_1_to_n])
general_forall_Py_if_Qy: 
In [6]:
general_nested_forall_Pxy_if_Qx = Forall(x_1_to_m,
Forall(y_1_to_n, P__x_1_to_m_y_1_to_n,
conditions=R__x_1_to_m_y_1_to_n),
conditions=Q__x_1_to_m)
general_nested_forall_Pxy_if_Qx: 
In [7]:
general_bundled_forall_Pxy_if_Qx = Forall((x_1_to_m, y_1_to_n),
P__x_1_to_m_y_1_to_n,
conditions=[Q__x_1_to_m, R__x_1_to_m_y_1_to_n])
general_bundled_forall_Pxy_if_Qx: 
In [8]:
general_forall__Py_not_T = Forall(y_1_to_n, NotEquals(P__y_1_to_n, TRUE))
general_forall__Py_not_T: 
In [9]:
general_forall__Py_not_T__st_Qy = Forall(y_1_to_n, NotEquals(P__y_1_to_n, TRUE),
conditions = [Q__y_1_to_n])
general_forall__Py_not_T__st_Qy: 
In [10]:
general_forall_st_Qx__Px_implies_Rx = Forall(x_1_to_n, Implies(P__x_1_to_n, R__x_1_to_n),
conditions=[Q__x_1_to_n])
general_forall_st_Qx__Px_implies_Rx: 
In [11]:
general_exists_Px = Exists(x_1_to_n, P__x_1_to_n)
general_exists_Px: 
In [12]:
general_exists_Px_st_Qx = Exists(x_1_to_n, P__x_1_to_n,
conditions=[Q__x_1_to_n])
general_exists_Px_st_Qx: 
In [13]:
general_exists_in_A_Px_st_Qx = Exists(x_1_to_n, P__x_1_to_n, domain=A,
conditions=[Q__x_1_to_n])
general_exists_in_A_Px_st_Qx: 
In [14]:
general_exists_Py = Exists(y_1_to_n, P__y_1_to_n)
general_exists_Py: 
In [15]:
general_exists_Py_st_Qy = Exists(y_1_to_n, P__y_1_to_n, conditions=[Q__y_1_to_n])
general_exists_Py_st_Qy: 
In [16]:
general_exists_Rz_st_Qz = Exists(z_1_to_n, R__z_1_to_n, conditions=[Q__z_1_to_n])
general_exists_Rz_st_Qz: 
In [17]:
general_exists_in_B_Py_st_Qy = Exists(y_1_to_n, P__y_1_to_n, domain=B,
conditions=[Q__y_1_to_n])
general_exists_in_B_Py_st_Qy: 
In [18]:
general_exists_notPx = Exists(x_1_to_n, Not(P__x_1_to_n))
general_exists_notPx: 
In [19]:
general_exists_notPx_st_Qx = Exists(x_1_to_n, Not(P__x_1_to_n),
conditions=[Q__x_1_to_n])
general_exists_notPx_st_Qx: 
In [20]:
general_notexists_Px = NotExists(x_1_to_n, P__x_1_to_n)
general_notexists_Px: 
In [21]:
general_notexists_Px_st_Qx = NotExists(x_1_to_n, P__x_1_to_n, conditions=[Q__x_1_to_n])
general_notexists_Px_st_Qx: 
In [22]:
general_notexists_Py = NotExists(y_1_to_n, P__y_1_to_n)
general_notexists_Py: 
In [23]:
general_notexists_Py_st_Qy = NotExists(y_1_to_n, P__y_1_to_n,
conditions=[Q__y_1_to_n])
general_notexists_Py_st_Qy: 
In [24]:
general_notexists_notPy = NotExists(y_1_to_n, Not(P__y_1_to_n))
general_notexists_notPy: 
In [25]:
general_notexists_notPy_st_Qy = NotExists(y_1_to_n, Not(P__y_1_to_n),
conditions=[Q__y_1_to_n])
general_notexists_notPy_st_Qy: 
In [26]:
%end common