How likely, and joined how? Degrees in ZTL¶

Vitaly Reznik

Say two statements are true with probability 0.3 and 0.7. Then "both are true" has no single probability. It is anything from 0 to 0.3, depending on how the two are joined, and the two numbers do not say how. Textbooks have known this since George Boole (1854) and Maurice Fréchet (1935). A common shortcut is to multiply, which assumes the statements are independent, and to leave that assumption unsaid. We did exactly that ourselves, as shown below.

ZTL, the logic this site is about, already has a name for a value that nobody has fixed: a dirty parameter. This page reads the unknown join of statements as one, and follows where that leads. No new theorem of probability is claimed: the bounds used are textbook ones (Fréchet, Markov). What is specific to ZTL is a check and some applications. The check: for a single connective on the inputs T, F and Z, its tables are exactly the "certain" end of these probability intervals. The applications: a lottery, a network of judges and a tree of judges. The rest is old mathematics applied with the assumption written down. One of the consequences is a correction to our own earlier work.

On this page proved marks a theorem checked in Lean 4, a proof assistant in which a machine checks every step. Each one uses none of Lean's three standard axioms (propext, Classical.choice, Quot.sound). Computed marks an exact calculation in fractions, by a program you can run. My reading marks what I take the results to mean. Open marks what is not settled.

Terms¶

A statement's degree is the probability that it is true: a number such as 0.3, or an interval such as [0.2, 0.4] when it is known only that far.
A joint distribution of several statements gives a probability to every combination of them being true or false. Each statement's own degree constrains it, but does not fix it.
With the joint unknown, a compound statement's degree is the interval over every joint that keeps each part's degree. For two parts these are the Fréchet bounds: P(a and b) lies in [max(0, a + b − 1), min(a, b)].
Independence is one particular joint: the product rule, P(a and b) = a·b. In ZTL it is a stipulation, a premise that is stated, never assumed by default.
A threshold is the probability a claim must reach. It is declared, too. There is no built-in 0.5.

ZTL's three values are read here as three degrees: T (true, checked) as [1, 1], F (false) as [0, 0], Z (not checked) as the whole [0, 1]. That reading is a modelling choice: it treats "not checked" as "nothing known about the probability".

What is already known¶

Boole (The Laws of Thought, 1854) and Fréchet (1935) gave the bounds above. Theodore Hailperin (Boole's Logic and Probability, 1976) put Boole's problem as linear programming. Nils Nilsson ("Probabilistic logic", 1986) built a logic on the same idea. Peter Walley's lower and upper probabilities (1991) are the general theory; the two ends of each interval here are a special case.
Henry Kyburg's lottery paradox (1961): for each ticket of a fair lottery it is rational to believe it loses, and the conjunction of those beliefs contradicts the rules.
Markov's inequality: if X ≥ 0, then P(X ≥ c) ≤ E[X]/c.
Lamport, Shostak and Pease (1982): a Byzantine fault-tolerant network of N nodes can agree as long as at most f = ⌊(N − 1)/3⌋ of them are compromised.

The tables of ZTL are the "certain" end of the degrees¶

A ZTL connective, such as "and", answers T only if T is forced under every way of reading its inputs. Otherwise it answers F. Read the inputs as degrees, with the join unknown, and ask when the lower end of the result's degree is 1: when every joint gives the result all its weight. For the inputs T, F and Z the extreme joints are exactly the classical readings, so there "lower end 1" and "true under every reading" are the same condition. The proof checks that ZTL's tables match it.

Proved. For every one- and two-argument connective and every input among T, F and Z, the ZTL table answers T exactly when that lower end is 1 (ZDegrees.projection, ZDegrees.projection1). The tables published in three places were checked against it cell by cell, and none differ: this site's 4 one-argument and 16 two-argument tables (4·3 + 16·9 = 156 cells), the author's own file of the 16 + 2 tables, and the code.

This holds per connective, not per formula. Composed node by node, the tables read "not (a and b)" with a, b unchecked as T: the inner "and" is not forced, so it answers F, and "not" then reads that F as a checked value and answers T. Yet one joint, with all the weight on "both true", gives "not (a and b)" degree 0 (proved, ZDegrees.compound_is_node_by_node). So a node-by-node T is not a verdict on the formula. The verdict ZTL gives a claim comes from its judge, which reads the whole formula: the claim is EARNED exactly when the whole formula's lower end is 1. For "not (a and b)" with a, b unchecked the judge does not say EARNED: it gives the value T, held ON CREDIT, meaning it rests on a and b, which nobody checked. This site's table pages list every cell where a composed table differs from the single connective. The judge's equivalence follows from the same fact about extreme joints. It is also computed, as a check of the two programs against each other, on 400 random formulas over 3 statements with every marking: 10 800 judgments, none differ.

My reading. On the inputs T, F and Z, ZTL's connectives are this probability logic seen at its coarsest grain. An F from a connective means "not earned", not "probably false". The proof covers only those three inputs. For a degree such as 0.3 the same rule is a definition, not a theorem: "not a" then has degree 0.7 and still answers F, because 0.7 is not 1. How likely a claim is gets said only against a threshold someone declares.

The lottery¶

Five tickets, one winner; each "ticket i loses" has degree 4/5. Computed:

claim	degree	at threshold 0.75
ticket 1 loses	4/5	EARNED
all five lose	[0, 4/5]	OPEN
all five lose, and some ticket wins	0	REFUTED
for contrast: all five lose, independence wrongly stipulated	1024/3125 ≈ 0.33	REFUTED

The lower end 0 is not a pessimist's artefact. The real lottery is one of the admissible joints: every ticket loses with probability 4/5 and "all lose" has probability 0. Independence would put "all lose" at a third. The tickets are not independent, since one win excludes the others.

My reading. Kyburg's rule "believe what is probable enough" fails under conjunction, and the degrees say where it fails: in the joint, which the rule never states.

A correction to our own work: a network of judges¶

In September we measured a network of judges that decide which facts to admit. We reported that below p = 1/3 (p is each judge's chance of being compromised), more judges make the network sharply safer: at p = 0.2, 0.819 with 4 judges and 0.998 with 90. Those numbers assumed that judges are compromised independently, and we did not say so. Correlated compromise is the case that matters: one shared bug, one vendor, one mistake in managing keys.

Here "the network holds" means the Byzantine model above: at most f of the N judges compromised. Compromise is counted, and no other failure is modelled.

Proved. With the joint of the compromises unknown, P(more than f of N compromised) ≤ N·p/(f + 1), so P(the network holds) ≥ 1 − N·p/(f + 1) (ZSwarmBounds.network_bound). This is a worst case over every joint, an adversarial one included. When N·p ≤ f + 1 the bound is attained: put weight on "f + 1 consecutive judges compromised, counting round the circle", equally for every starting judge, and the rest on "none". Every judge then has probability exactly p. The theorems attained_4, attained_30 and attained_90 check this with equality at p = 1/10; for other p the construction is the same but is not checked in Lean.

p	N = 4	N = 30	N = 90	independent: N = 4 / 30 / 90
0.10	0.80	0.70	0.70	0.948 / 0.9995 / 1.000
0.20	0.60	0.40	0.40	0.819 / 0.939 / 0.998

My reading. With the joint unknown, the worst-case guarantee tends to 1 − 3p as N grows. It is not monotone in N, because f is rounded down: at p = 0.1 it is 0.70 with 3 judges and 0.80 with 4. Beyond a handful of judges, adding more does not raise it; here it falls from 0.80 at 4 judges to 0.70 at 30 and 90. What the strong numbers depend on is the independence of the judges' failure domains: different code, different operators, different keys. That independence, or some partial structure in between, has to be established or stated as a premise. It should not be assumed in silence.

A tree of triples, and what a lottery of seats buys¶

A swarm can decide a fact without a centre: 81 seats in groups of three, each group deciding 2 of 3, and the results grouped in threes again up to one verdict. It was already proved that capturing the tree takes at least 16 liars placed right (ZMajority.lie_needs). With Markov's inequality this gives, for every joint of the liars, P(capture) ≤ 81p/16, about 5p (proved, ZSwarmBounds.tree_bound).

81 seats, each seat lying with probability p. The first column is the proved bound, capped at 1; it is an upper bound, and whether it is attained at 81 seats is not checked. The second is computed exactly: for each number k of liars, the share of the k-seat sets that capture the tree is counted by dynamic programming over the tree, and the worst mixture of k with mean 81p is then found. The third is the independent case, computed exactly.

p	seats fixed, liars' joint unknown (bound)	seats drawn by lot, liars' joint unknown	liars independent
0.01	0.051	0.016	1.4 × 10⁻²⁵
0.10	0.506	0.160	7.6 × 10⁻¹⁰
0.30	1	0.481	4.6 × 10⁻³

With fixed seats, an adversary who knows them and coordinates the liars reaches the bound. That is computed on a 27-seat tree; it is not proved for 81. Drawing the seats by lot gains about a factor of 3 at small p, and less as the values saturate (about 2 at p = 0.3). It helps only if the liars are fixed before the draw. While p is small, capture still grows in proportion to p. Only independent liars give the tiny numbers in the last column.

My reading. There are two kinds of independence here, and they are not alike. The lottery of seats is independent of the liars because we build it so, on one condition: the draw comes after the liars are fixed (for example from randomness published later by a source the adversary cannot predict or bias). Checking it needs a trusted record of when the liars were fixed; that is a trust assumption of its own, but a narrower one. The liars' independence of each other is a claim about the world, and it can only be stated as a premise.

Independence between groups¶

That example needs something between "all independent" and "nothing independent": the draw is independent of the liars, while the liars' own joint stays unknown. ZFL, the table language in which claims are given to the ZTL judge, now takes groups. In a ZFL document the field independent is either true or a list of groups such as [["a", "b"], ["c"]]. The groups are independent of one another, and the joint inside a group stays unknown. With a, b and c each at 1/2, "a and b and c" has the following degree (computed):

[0, 1/2] with the joint unknown;
1/8 with all three independent;
[0, 1/4] with the groups {a, b} and {c}.

The computation is exact. The probability is multilinear in the groups' distributions: fix all groups but one and it is linear in that one. So its ends lie at corners of each group's set of distributions, and the program enumerates them. That enumeration grows quickly with group size, so it is limited: every group except the largest may hold at most 3 statements, and a claim at most 10 events. A statement left out of every group is refused, not guessed. You can try it in the studio.

Open¶

A statement outside every group: its joint with all the others is unknown, and that mixed case is not computed yet.
An adversary who sees the draw of seats: the table's middle column does not cover it.
That the tree bound is attained is computed on 27 seats; it is not proved in Lean.
Statements about incompatible quantum observables have probabilities within each measurement context, but no single joint distribution reproduces the quantum predictions across contexts (Bell, Hardy, Kochen–Specker). The Fréchet set presumes such a joint, so degrees across incompatible contexts do not apply.

The code¶

All of it is in the public ZTL repository, github.com/inventor1975/ZTL:

lean/ZDegrees.lean: the tables as thresholds of degrees. 14 theorems, no axioms.
lean/ZSwarmBounds.lean: the network bound, its attainment, and the tree bound. No axioms.
lean/ZMajority.lean: the tree of triples, including lie_needs.
Each of these three Lean files prints #print axioms for its main theorems, and the repository's axiom audit checks every theorem in them.
zdegree.py: exact degrees by linear programming in fractions. Each end is certified twice, by a distribution that attains it and a dual that bounds it. Partial independence is degree_groups.
ztlnetwork.py, zswarm_bounds.py, dilemmas/lottery.py: the tables above, each a test that asserts its numbers.
SPEC.md, section "Degrees", and in the ZFL language the fields degree, need and independent. Try them in the studio.

Written with AI assistance (Claude Opus 5.5, Anthropic): the theorems, programs and this text. Idea, direction, editing and responsibility: Vitaly Reznik.