SQEMA with universal and polyadic modalities

Modal Formula:

Current Formula:


First-Order Formula:


Proof:

Log:

Modal Formulas Legend: Nominals: starting with a small Latin 'c', alphanumeric. Propositional Variables: starting with a small Latin letter other than 'c', alphanumeric. `# - -` Necessity, syntax: `#A` or `#(A₁, ..., A_k)` `@ - -` Possibility, syntax: `@A` or `@(A₁, ..., A_k)` `#' - ^-1 -` Reversed Necessity; also: %, syntax: `#'A` or `[0 -L](A₁, ..., A_k)` for `1 ≤ L ≤ k` `@' - ^-1 -` Reversed Possibility; also: ^, syntax: `@'A` or `<0 -L>(A₁, ..., A_k)` for `1 ≤ L ≤ k` `[U] -` Universal necessity `<U> -` Universal possibility `[n] -` Necessity with relation index, where n is a number, syntax: `[n]A` or `[n](A₁, ..., A_k)` `<n> -` Possibility with relation index, where n is a number, syntax: `<n>A` or `<n>(A₁, ..., A_k)` `[n]'-` Reversed Necessity with relation index, where n is a number, syntax: `[n]'A` or `[n -L](A₁, ..., A_k)` for `1 ≤ L ≤ k` `<n>'-` Reversed Possibility with relation index, where n is a number, syntax: `<n>'A` or `<n -L>(A₁, ..., A_k)` for `1 ≤ L ≤ k` `& - -` Conjunction `\| - -` Disjunction `~ - -` Negation `-> -` Implication `<- -` Reversed Implication `<-> -` Equivalence `+ - -` Exclusive-Or (XOR) `0 - -` False `1 - -` True Pre-Contact Formulas Legend: Propositional Variables: starting with a small Latin letter, alphanumeric. `0 -` Boolean Zero `1 -` Boolean One `- -` Unary Complement `* -` Boolean Intersection `+ -` Boolean Union `F - -` False `T - -` True `C -` Contact, syntax: `C(T₁, T₂)` `== -` Equality `<= - ≤ -` Part Of `<` `>= - ≥` `>` `& - -` Conjunction `\| - -` Disjunction `~ - -` Negation `-> -` Implication `<- -` Reversed Implication `<-> -` Equivalence