Lingenic

# LINGENIC
# A notation for knowledge. Self-describing.

# ═══════════════════════════════════════════════════════════════
# WHAT
# ═══════════════════════════════════════════════════════════════

notation(Lingenic) ∧ ¬programming_language(Lingenic) ∧ ¬ontology(Lingenic)

purpose(Lingenic) ≜ combine(structure, content)
structure ≜ mathematics
content ≜ natural_language

# ═══════════════════════════════════════════════════════════════
# PRINCIPLES
# ═══════════════════════════════════════════════════════════════

compose(known_primitives) ∧ ¬invent(new_symbols)
use(math, for(structure)) ∧ use(language, for(content))
∀symbol ∈ Unicode_mathematical_operators: valid(symbol)
∀lang ∈ human_languages: compatible(Lingenic, lang)

# Lingenic describes knowledge. Querying and commanding are the reader's job.

# ═══════════════════════════════════════════════════════════════
# ATOMS
# ═══════════════════════════════════════════════════════════════

# Predication — the fundamental form
form(statement) ≜ predicate(arguments)

loves(Alice, Bob)
on(the cat, the mat)
said(Marie, "bonjour")
住んでいる(田中, 東京)

# ═══════════════════════════════════════════════════════════════
# OPERATORS — ALL FROM UNICODE, ALL STANDARD
# ═══════════════════════════════════════════════════════════════

# Propositional logic — Frege 1879, Peano 1889, Russell 1910
∧ ∨ ¬ → ← ↔ ⊕ ⊤ ⊥

# Modal operators — Lewis 1918, Kripke 1959
□ ◇

# Quantifiers — Frege 1879, Gentzen 1935
∀x ∃x ∃!x ∄x

# Set theory — Cantor 1874, Peano 1889
∈ ∉ ⊂ ⊃ ⊆ ⊇ ∪ ∩ ∅ {a, b} {x: P(x)}

# Relations — standard mathematics
= ≠ < > ≤ ≥ ≈ ≡ ∝ ≺ ≻ ≼ ≽ ≲ ≳ ≬ ⊏ ⊐ ...

# Arrows — standard mathematics
→ ← ↔ ⇒ ⇐ ⇔ ↦ ⟶ ⟷

# Arithmetic — standard mathematics
+ − × ÷ · / √ ∛ Σ ∏ ∫ ∂ ∇ ⌊⌋ ⌈⌉

# Proof theory — Gentzen 1935
⊢ ⊨ ∴ ∵

# Definition — standard mathematics
≜

# Number sets — Bourbaki 1939
ℕ ℤ ℚ ℝ ℂ
⁰¹²³⁴⁵⁶⁷⁸⁹ⁿ ₀₁₂₃₄₅₆₇₈₉ₙ

# Lambda calculus — Church 1936
λx.M            # function abstraction
(λx.M)N         # application

# Type theory — Church 1940, Martin-Löf 1972
x : T           # x has type T
A → B           # function type
A × B           # product type
A + B           # sum type
Πx:A.B          # dependent product
Σx:A.B          # dependent sum

# Dynamic logic — Pratt 1976, Harel 1979
[α]P            # after all executions of α, P holds
⟨α⟩P            # after some execution of α, P holds
α;β             # sequential composition
α∪β             # nondeterministic choice
α*              # iteration
?P              # test: proceed if P, else fail — within program descriptions only

# Relational algebra — Codd 1970
⟕               # left outer join  (statement primary, metadata supplements)
⟗               # full outer join  (merge two knowledge bases)

# ═══════════════════════════════════════════════════════════════
# COLLECTIONS
# ═══════════════════════════════════════════════════════════════

{a, b, c}        # set — unordered, no duplicates
[a, b, c]        # list — ordered, duplicates allowed

a ≜ [x, y, z]
a₀ = x  ∧  a₁ = y  ∧  aᵢ = i-th element

# ═══════════════════════════════════════════════════════════════
# DEFINITIONS
# ═══════════════════════════════════════════════════════════════

mortal(x) ≜ ∃t(dies(x, t))
bachelor(x) ≜ male(x) ∧ adult(x) ∧ ¬married(x)
even(n) ≜ ∃k ∈ ℤ. n = 2k
GDP ≜ gross_domestic_product

# Definitions expand
bachelor(John) → male(John) ∧ adult(John) ∧ ¬married(John)

# ═══════════════════════════════════════════════════════════════
# MODALITY — STANDARD NOTATION BY DOMAIN
# ═══════════════════════════════════════════════════════════════

# Modal logic — Lewis 1918, Kripke 1959
□P              # necessarily P
◇P              # possibly P

# Linear Temporal Logic (LTL) — Pnueli 1977
GP              # globally / always
FP              # future / eventually
XP              # next
HP              # historically / always in past

# Epistemic logic — Hintikka 1962
KₐP             # agent a knows P
BₐP             # agent a believes P

# Deontic logic — von Wright 1951
OP              # obligatory
PP              # permitted
FP              # forbidden

# Counterfactual conditionals — Lewis 1973
P □→ Q          # if P were, Q would be

# ═══════════════════════════════════════════════════════════════
# PROBABILITY — Kolmogorov 1933
# ═══════════════════════════════════════════════════════════════

P(rain) = 0.7
P(wet | rain) = 0.99
P(X) ∈ [0.6, 0.8]

# ═══════════════════════════════════════════════════════════════
# CAUSATION
# ═══════════════════════════════════════════════════════════════

# Counterfactual theory — Lewis 1973
¬smoking □→ ¬cancer
watered(plant) □→ alive(plant)

# Interventionist theory — Pearl 2000
P(cancer | do(smoke)) > P(cancer | do(¬smoke))
P(alive | do(water)) > P(alive | do(¬water))

# ═══════════════════════════════════════════════════════════════
# TIME
# ═══════════════════════════════════════════════════════════════

# Process algebra — Hoare 1978 (CSP), Milner 1980 (CCS)
P ; Q           # sequential composition
P ∥ Q           # parallel composition

# Interval relations — Allen 1983
before(P, Q)  ∧  after(P, Q)  ∧  meets(P, Q)  ∧  during(P, Q)  ∧  overlaps(P, Q)

at(event, t)
during(event, [t₁, t₂])

# ═══════════════════════════════════════════════════════════════
# METADATA — Codd 1970 (relational algebra)
# ═══════════════════════════════════════════════════════════════

# Left outer join: statement is primary, metadata record supplements it.
statement ⟕ {key: value, key₂: value₂}

□(E = mc²) ⟕ {src: Einstein, year: 1905}
P(rain) = 0.7 ⟕ {src: forecast}

# Agent assertion — proof-theoretic (Gentzen 1935)
# Use when attribution carries derivation/endorsement semantics.
Alice ⊢ P(rain) = 0.8

# Reification — for metadata about metadata, name the statement first.
φ₁ ≜ □(E = mc²)
src(φ₁, Einstein) ∧ year(φ₁, 1905) ∧ P(φ₁) = 1.0

# Knowledge base merge — full outer join
knowledge_base_A ⟗ knowledge_base_B

# ═══════════════════════════════════════════════════════════════
# CONTEXTS — SET MEMBERSHIP
# ═══════════════════════════════════════════════════════════════

(E = mc²) ∈ physics
(e = 2.71828...) ∈ math
(E ≜ eggs) ∈ cooking

{E = mc², F = ma, c = 299792458} ⊂ physics

E ∈ physics ≠ E ∈ cooking

# ═══════════════════════════════════════════════════════════════
# MULTILINGUAL
# ═══════════════════════════════════════════════════════════════

∀x(human(x) → mortal(x))           # English
∀x(人間(x) → 死ぬ(x))               # Japanese
∀x(человек(x) → смертен(x))        # Russian
∀x(إنسان(x) → فانٍ(x))             # Arabic

# Structure invariant. Content transforms.

# ═══════════════════════════════════════════════════════════════
# GRANULARITY
# ═══════════════════════════════════════════════════════════════

happened(something, yesterday)

sat(cat, mat)

sat(the_orange_tabby, on(the_mat)) ∧ at(this, 2024-01-15T14:00Z)

sat(entity(cat, id=C001, mass=4.2kg), on(entity(mat, id=M001)))
⟕ {observed_by: camera_3, P: 0.99}

# ═══════════════════════════════════════════════════════════════
# EXAMPLE — COMPLETE
# ═══════════════════════════════════════════════════════════════

mortal(x) ≜ ∃t(dies(x, t))

premise₁ ≜ □(∀x(human(x) → mortal(x)))
premise₂ ≜ human(Socrates)

premise₁ ∧ premise₂ ⊢ mortal(Socrates)
⟕ {by: modus_ponens, P: 1.0, src: Aristotle}

# ═══════════════════════════════════════════════════════════════
# READING
# ═══════════════════════════════════════════════════════════════

predicate(args)         ≡ relation(predicate, arguments)
∀x(P(x))               ≡ universal_quantification
∃x(P(x))               ≡ existential_quantification
P → Q                   ≡ implication
P ∧ Q                   ≡ conjunction
statement ⟕ {metadata}  ≡ annotated_statement
source_A ⟗ source_B     ≡ merged_knowledge_bases
(P) ∈ context           ≡ scoped_statement
x ≜ y                   ≡ definition
[a, b, c]               ≡ ordered_sequence
[α]P                    ≡ after_all_executions_of_α_P_holds
?P within [α]           ≡ test_within_program (dynamic logic only — not a query)

# ═══════════════════════════════════════════════════════════════
# SUMMARY
# ═══════════════════════════════════════════════════════════════

Lingenic ≜ (
    structure ≜ mathematics ∧
    content ≜ natural_language ∧
    operators ⊂ Unicode ∧
    descriptive ∧ ¬query_language ∧ ¬command_language
)