// logic_background
From Aristotle to possible worlds — my academic background in logic, studied at the Universidad Nacional de Córdoba.
// alma_mater
I studied logic as a formal academic discipline at the Universidad Nacional de Córdoba (UNC) — founded in 1613, it is one of the oldest and largest universities in Latin America, and consistently ranked among the top in the region.
My specialization wasn't just programming logic. It was the philosophical and mathematical foundations of reasoning itself — the kind of thinking that asks: what makes an argument valid? What does it mean for something to be necessarily true? Can a system of reasoning be both consistent and complete?
These questions shaped how I approach code, design, and problem-solving. Logic isn't just a subject I studied — it's a lens I think through.
Especialización en Lógica
Universidad Nacional de Córdoba
Córdoba, Argentina
// topics_studied
Ten disciplines that shaped a rigorous way of thinking.
Classical Logic
Syllogisms, the square of opposition, and categorical propositions — the ancient foundation of formal reasoning dating to 350 BC.
// example_syllogism
Propositional Logic
Truth tables, logical connectives (∧ ∨ ¬ →), tautologies, and the algebra of propositions. The backbone of Boolean reasoning.
// truth_table P → Q
Predicate Logic
Universal (∀) and existential (∃) quantifiers extend propositional logic to reason about properties and relations between objects.
// universal_statement
First-Order Logic (FOL)
Extends predicate logic with function symbols and constants. Gödel's Completeness Theorem (1930) proved FOL is sound and complete — every semantic truth has a proof.
// key_theorem
Second-Order Logic
Quantifies over predicates and functions — not just individuals. Far more expressive than FOL, but at a cost: it loses completeness and compactness.
// second_order_quantification
Quantifier Theory
Deep study of quantifier scope, bound vs. free variables, substitution rules, and the semantic interpretation of quantified sentences.
// scope_matters
Argumentation Theory
Fallacies (ad hominem, straw man, false dilemma), the Toulmin model of argument, and rhetoric — reasoning in natural language contexts.
// toulmin_model
Paraconsistent & Many-Valued
Łukasiewicz 3-valued logic, fuzzy logic, and paraconsistent systems that tolerate contradictions without exploding into triviality.
// 3-value logic (T, I, F)
Temporal Logic
Modal operators for time: ◻ (always/globally), ◇ (eventually), ○ (next), U (until). Used in formal verification, model checking, and AI planning.
// temporal_operators
Set Theory (ZFC)
Zermelo-Fraenkel axioms with the Axiom of Choice. Cantor's diagonalization, infinite cardinalities (ℵ₀, ℵ₁), power sets, and the foundations of mathematics.
// set_operations
// possible_worlds_semantics
The most captivating area of my logic studies — a framework for necessity, possibility, and truth across multiple worlds.
In modal logic, we extend classical propositional logic with two operators:
□P is true at a world w if P is true in all worlds accessible from w.
◇P is true at a world w if P is true in at least one world accessible from w.
A Kripke frame is a pair ⟨W, R⟩ where W is a set of possible worlds and R ⊆ W × W is an accessibility relation between them. A model adds a valuation function V that assigns truth values to propositions at each world.
Worlds W1, W2, W3 connected by accessibility relation R. Proposition P is true in W1 and W2, but false in W3.
Since R = {(W1,W2), (W2,W3)}, □P holds at W2 (all accessible worlds satisfy P), but □P does not hold at W1 (W3 is reachable via W2 and fails P in the transitive sense).
In a T-frame (System T), the accessibility relation is reflexive: every world can see itself. This encodes the axiom □P → P — what is necessary is actual.
The T-frame axiom □P → P (what is necessarily true, is true) requires reflexivity. System S4 adds transitivity; System S5 adds symmetry — giving the full logic of alethic necessity used in analytic philosophy.
Temporal logic uses a tree structure where the past is linear but the future branches. At each moment, multiple possible futures exist until one becomes actual.
In branching time temporal logic (CTL), ◇P means "there exists a branch where P eventually holds." The formula AG(P) — in all branches, P always holds — is the branching-time analog of □P.
Given: W = {w₁, w₂, w₃}, R = {(w₁,w₂), (w₂,w₃)}, P is true in w₂ and w₃. Is □P true at w₁?
// worlds accessible from w₁: {w₂}
// check P at each: P(w₂) = T ✓
// all accessible worlds satisfy P
Only w₂ is directly accessible from w₁, and P holds there. So □P holds at w₁.
Same model. Is ◇□P true at w₁?
// ◇□P at w₁: ∃w accessible from w₁ where □P holds
// check □P at w₂: accessible from w₂ = {w₃}, P(w₃) = T ✓
// so □P holds at w₂ — which is accessible from w₁ ✓
w₂ is accessible from w₁, and □P holds at w₂ (since all worlds accessible from w₂, namely w₃, satisfy P). So ◇□P is satisfied.
Branching time. In the tree diagram above, at t₀ is ◇□P true? Is □◇P true?
// ◇□P: does some branch lead to a point where P is always true?
// branch α → t₂ₐ (P=T) → t₃ₐ (□P) — YES, □P holds at t₃ₐ ✓
// □◇P: on ALL branches, does P eventually hold?
// branch β → t₂ᵦ (P=F) → t₃_c (¬P) — NO, P never holds ✗
In branching time, ◇□P and □◇P behave differently — branch α makes P necessarily true eventually, but branch β never achieves P, so universal inevitability fails.
// logic_meets_code
Formal reasoning isn't separate from writing software — it's the substrate underneath it.
Every TypeScript type is a predicate over values. Generics are universal quantifiers. Conditional types are implications. The type checker is a proof engine — it verifies that your claims about data hold across all possible inputs.
The React component lifecycle is a temporal sequence: mount → update → unmount. State machines in XState are directly modeled by Kripke structures — states are worlds, transitions are the accessibility relation, guards are valuations.
Arrays, Maps, Sets — all data structures are sets with operations. Union (∪) is merge, intersection (∩) is filter, difference is exclude. Understanding cardinality and set properties helps reason about time complexity and data transformations.
A bug is a false proposition in your mental model of the code. Debugging is finding which premise in your reasoning chain is wrong. Truth tables help exhaustively check edge cases — the kind of systematic thinking that prevents "it works on my machine" bugs.