INFERENCE PROTOCOLS // CORE LOGIC

The archive groups every core operation into nine protocol classes.
Each block below shows the operation, its formal shape, and the reasoning it trains.

Negation and Equivalences

Operation	Formula	Explanation
Statement negation	¬P	Marks that a claim is not true.
Double negation	¬¬P ⇔ P	Two negations return the statement to its original truth.
De Morgan's laws	¬(A ∧ B) ⇔ (¬A ∨ ¬B)	Negating a conjunction turns into at least one negated branch.

Implication and Deduction

Operation	Formula	Explanation
Implication	A → B	Reads as "if A, then B" and fixes the direction of the claim.
Modus ponens	A → B, A ⊢ B	If the condition holds and the rule is true, the consequence follows.
Modus tollens	A → B, ¬B ⊢ ¬A	If the consequence fails, the original condition cannot have held.

Quantifiers

Operation	Formula	Explanation
Universal quantifier	∀x P(x)	Applies one rule to every member of a class.
Existential quantifier	∃x P(x)	Confirms that at least one valid instance exists.
Negated existential	¬∃x P(x)	States that no instance exists that satisfies the predicate.
Non-empty class plus universal rule	∃x A(x) ∧ ∀x(A(x)→B(x)) ⊢ ∃x(A(x)∧B(x))	Combines existence with a universal rule to prove a concrete overlap.

Temporal Quantifiers

Operation	Formula	Explanation
Universal temporal quantifier	∀t P(t)	Claims that the predicate holds at every relevant time.
Existential temporal quantifier	∃t P(t)	Claims that the predicate holds at least once in time.
Ban on simultaneity	¬(A ∧ B)	Used with exclusive choices to forbid both states at once.
Temporal implication	A → ◇B	A trigger makes a later or possible outcome logically available.

Logical Connectives

Operation	Formula	Explanation
Conjunction	A ∧ B	Both linked statements must hold together.
Inclusive disjunction	A ∨ B	At least one branch is true, and both may still be true.
Exclusive disjunction	A ⊕ B	Exactly one branch may hold, never both together.

Relations and Property Transfer

Operation	Formula	Explanation
Transitivity	(A→B) ∧ (B→C) ⊢ (A→C)	Chains two valid implications into a longer valid consequence.
Shared property	∃x(A(x) ∧ X(x)) ∧ ∃y(B(y) ∧ X(y))	Shows that both classes instantiate the same property without proving they are equivalent.
Incompatibility	A → ¬B	Declares that once A holds, B is ruled out.

Classes and Subclasses

Operation	Formula	Explanation
Class membership	A ∈ B	Places one object inside a named class.
Subclass relation	A ⊂ B	Shows that one class is contained inside a broader class.

Metalogic

Operation	Formula	Explanation
Insufficient information	?	No forced conclusion is available from the evidence given.
Contradiction	A ∧ ¬A	A report breaks when it asserts a statement and its negation together.
False implication	A→B ≠ B→A	The consequence of a rule cannot be reversed without proof.
Excluded middle	P ∨ ¬P	A statement is either true or false inside the forced domain.

Fallacy Detection

Operation	Formula	Explanation
Affirming the consequent	A→B, B ⊬ A	Seeing B does not prove that A caused it.
Denying the antecedent	A→B, ¬A ⊬ ¬B	Removing the trigger does not automatically remove the outcome.
Contraposition	A→B ≡ ¬B→¬A	The valid reverse form of implication negates both sides.
Disjunctive syllogism	A∨B, ¬A ⊢ B	If one branch of an either-or is false, the other branch remains.
Exception handling	∀x(¬E(x) → P(x))	A rule may hold generally while still reserving a specific exception set.