Reasoning about Chance: Proof Theory for Aleatoric Logic Tim French 0 The University of Western Australia

Aleatoric Logic is a logic of chance, where the interpretation of propositional atoms is modelled as the flip of a coin, or a marble drawn from an urn. Propositions correspond to these chance events and consequently their interpretation is inherently probabilistic. Propositions are not evaluated as true or false, but instead are evaluated as likelihoods, giving a many-valued logic similar to fuzzy logics. An equational theory is given through an equivalence relation that associates two propositions with identical likelihood: for example the chance of a coin landing heads and then tails, will be the same as the chance of the coin landing tails and then heads, regardless of the coin's bias. In this paper we present a refined syntax for aleatoric logic and provide a proof system for the equational theory.

 eol>Probabilistic Reasoning Aleatoric Logic Proof Theory 1. Introduction 2. Related work

There has been a considerable number of works that have examined the semantics of probability. Early work includes Kolmogorov [ 3 ], Ramsey [ 4 ] and de Finneti [ 5 ], who produced axioms for reasoning about probabilities of events. There have been a number of very good works that have examined logics of probabilistic reasoning, including [ 6, 7, 8, 9 ]. These approaches include a modality for the probability of some event occurring. As the probabilities are explicit in the syntax, these approaches reason about the probabilities of events: compare the certain statement route 1 is faster 80% of the time to the uncertain statement route 1 is faster. The first is about an explicit probability and is always true or false, whilst the second is a probabilistic statement that may be sometimes true and sometimes false.

Fuzzy logics and many valued logics take a similar many valued approach to reason about linguistic variables in the presence of vagueness [ 10, 11, 12, 13 ], where the semantics allow for the increasing or decreasing of plausibility, without necessarily committing to the absolute certainty of a proposition. When the product semantics are used (so the plausibility of two propositions taken together are multiplied) there is some correspondence with independent random events like the flipping of coins, although the semantics are not entirely probabilistic: the residual operator has no probabilistic analogue and complementation does not represent the failure of an event to occur. An axiomatization of the Basic Logic BL is given and extended to various settings and forms including first order logics. While the underlying fuzzy logic is many valued, BL axiomatises the set of propositions whose interpretation is necessarily true (or equal to 1). Rational Pavelka Logic [ 14 ] introduces a set of rational constants between 0 and 1 to the language, and is able to extend the axiomatization BL to the set of propositions necessarily greater than some threshold. In [ 13 ] Majer and Sedlár introduce a many valued probabilistic modal logic, that is an extension of Łukasiewicz logic.

An equational proof theory has previously been presented for the aleatoric calculus and aleatoric modal calculus. These logics are substantially simpler than the one we investigate here, as they do not include the fixed point operator introduced in [ 1 ].

3. Aleatoric Propositions

Here we present a syntax and semantics for describing aleatoric propositions, and their probabilities.

The essential elements of the language are a set of propositional atoms corresponding to some proposition, and operations describing propositions built from these elements (negation, conjunction, iteration).

3.1. Syntax Definition 1.

form: For the syntax we assume a set of propositional atoms = {, , , . . . }, corresponding to propositions.

The syntax for ℒ, the language of aleatoric propositions, is given by the Backus-Naur ℒ = ::= | ¬ | ∧ | ◁▷ | F. where ∈ , and in the proposition F. , must be linear in : an atomic proposition ∈ is linear in if and only if for every sub-formula ∧ of , does not appear in . Any propositional atom that does not only appear within the scope of F operators in is free in and we let fr() refer to the set of free variables in . Parentheses will be used to indicate precedence.

The propositions are conceived of as events of chance: every separate occurrence of an atom is considered as a flip of a biased coin, or a Bernoulli test. The operations are built recursively so that every proposition may be considered to be a complex Bernoulli test, as follows: • ¬ (not ) inverts the outcome of the test, so success is replaced by failure and vice-versa • ∧ ( and ) is a test that passes if and only if the test for passes and the test for passes. • ◁▷ , ( or ) is a test that randomly and fairly chooses either or to test, and passes if and only if the chosen test passes1. • F. , corresponding to a test where every evaluation of the atom is replaced by the original proposition, F..

The fixed point operator, F. , required that is linear in , and this is to ensure that the fixed point is unique and non-ambiguous. This is a similar notion to monotonicity, which is used when defining ifxed points in discrete domains.

We use the abbreviations ∨ for ¬(¬ ∧ ¬) and → for ¬( ∧ ¬). 1The choice of the term “or” will no doubt be controversial as it clashes with the familiar term for logical disjunction. However, arguably the common usage of the term is just as good a match for this aleatoric or.

For example, consider the proposition:

F.(( ∧ ) ◁▷ ( → )) This is interpreted as a test where a random choice is made between the left and right arguments of◁▷. If ∧ is chosen then the test is performed. If it fails, the whole proposition fails, while if it passes, we must test which is a proxy for repeating the test from the beginning. On the other hand, if the right argument, → is chosen, then if the test for fails, the whole proposition passes, while if passes then we must test so we repeat the test from the start.

 3.2. Semantics

The semantics describe the likelihood of a proposition given an interpretation, where an interpretation simply assigns likelihoods to atoms.

Definition 2. An interpretation is a map I : →− [ 0, 1 ] that assigns a probability to each variable. Given an interpretation, I, let I[← ] be the interpretation where for all ∈ , I[← ] ( ) = I( ) if ̸= , and I[← ] () = .

Definition 3. The interpretation, I may be extended to the whole of ℒ as follows 2:

I (¬) I

I ( ∧ ) ( ◁▷ ) (F.) I (F.) I = I() = 1 − I = I · I I = ( I + I)/2 =

1/2 if I[1←/2] = where I[←] = 1/2, and = , otherwise.

We call I the I-likelihood of , or just likelihood of when I is clear from context.

The semantics are similar to fuzzy logic [ 10, 11 ], with the product T-norm, but there is no notion of a residual, and the negation operator is quite diferent. The operators and propositions act as elements in a chance driven protocol, with atomic propositions being elements of pure chance, ¬ is the chance of the test failing, ∧ is the chance of and passing, noting that each occurrence of and is an independent event, ◁▷ is the chance of a random choice of or passing, and F. is the chance of , where is interpreted as having the same chance as F. . The fact that is linear in is suficient to ensure that (F.) I is always uniquely determined.

Lemma 4. In all interpretations I, for all propositions F. , the I-likelihood of F. is always uniquely defined.

Proof: (Sketch) To see this, it is enough to notice that when is linear in , and does not contain any fixed point operators, then I may always be written as

(1I, . . . , I) + (1I, . . . , I) · I where the 1, . . . , , are the variables of , and and are polynomial functions, such that for all interpretations (1I, . . . , )I) + (1I, . . . , I) ≤ 1 . Therefore, the evaluation of (F.) I is the solution to the equation: = (1I, . . . , I) + (1I, . . . , I) · , so, (F.) I = (1I, . . . , I) 1 − ( 1I, . . . , I) . 2The split for (F.) I is to account for the case where = , and there are infinitely many fixed points. See the proof of Lemma 4.

(( ∧ ) ∨ ) ◁▷ (( → ) ∧ ) ((¬ ∧ ) ∨ ) ◁▷ ((¬ → ) ∧ ) ◁▷ ⎞I ⎠ = ( I · I + (1 −

· I) I)/4 as required. as: ⎛ ⎝

(( ∧ ) ∨ ) ◁▷ (( → ) ∧ ) ((¬ ∧ ) ∨ ) ◁▷ ((¬ → ) ∧ )

◁▷ Solving for the fix point we have: Note if the denominator of this equation is 0, then the equation is efectively = , so every value is a solution, and particularly = 1/2 is a solution, so we would have (F.) I = 1/2. If alpha does contain fix point operators, then we can apply this argument inductively, where and are now rational functions, noting that the linearity constraint is enough to ensure that the denominator would always be functionally independent of I.

, which was taken as a primitive in the earlier work. (? : )

I = I · I + (1 −

I) I, · so is tested, and if it holds, the proposition is interpreted as and if it fails the proposition is interpreted as . It is non-trivial to deduce this interpretation so we derive it here. The subformulas are evaluated (( ∧ ) ∨ ) ((¬ ∧ ) ∨ ) (( → ) ∧ ) (((¬ → ) ∧ )

I I I I = I · I + (1 −

· I I

) · I = I = (1 −

− = ( I + I −

I · I + (1 − I + I I ·

· I I ) · I ) · I

I + I · I) · The aleatoric or operators take a uniformly weighted sum of the formulas (each is multiplied by 1/4): ⎞I ⎠ ⎡ I · I + (1 −

· I I

) · I = ∑︁ ⎢ I − ⎢⎣ (1 − ( I + I −

I · I + (1 − I + I I ·

· I I ) · I

) · I = ( I · I + (1 −

I) · I + 3 · )/4

I + I · I) · ⎥⎥ /(42) □ ℒ

Within the minimal language, ℒ, we are able to describe some interesting non-aleatoric properties. Particularly ⊤ is the event that always happens, or in traditional terms: true. Correspondingly ⊥ is the event that never happens, or false. These abbreviations are then important in defining logical operators such as conjunction, disjunction, and implication, although care must be taken with these operators as their operands are aleatoric. For example, = ∧ ( → ) □ that must occur twice in this equation. Indeed, expanding it out we find I = I ·( I · I +1−

I ) ̸= I.

On the other hand 1/2 is entirely aleatoric and represents pure random chance. Finally, the operation allows us to determine whether a formula is always Yes. We use the operator and language of modal logic here, using the box operator to indicate that alpha is necessary. This is not a modal interpretation, and there are no possible worlds, although one could make the analogy that each time an atom is is not equivalent to , since is an event sampled corresponds to a possible world.

 4. Aleatoric Logic

The aleatoric propositions described so far do not conform to the standard definition of a logic, which is, roughly, a set of true statements in a given language. The aleatoric propositions given an inherently probabilistic many valued logic. In the case of Fuzzy Logics like the Basic Logic [ 11 ], MTL ([ 15 ] and RPL [ 14 ] have provided recursive axiomatisations of the sets of propositions that are always true. However in the context of aleatoric logic, such a set would not be very interesting, as none of these propositions would contain an element of chance.

To build a logic of aleatoric propositions we must introduce an unambiguous relationship between propositions, and the simplest relationship is equivalence, to mean that two propositions have identical chance.

4.1. Identities Definition 5.

identities. with the intended meaning that and have exactly the same likelihood. Let Ξ be the set of all aleatoric An aleatoric identity is a pair of aleatoric propositions , ∈ ℒ , and is denoted ≃ , satisfied by all interpretations, we say it is a valid identity.

Given some interpretation, I, we say I em satisfies the identity ≃ if I = I. If an identity is

With the concept of identity we are able to go beyond the extensional interpretation of what is observed, to the intensional interpretation of which propositions are equivalent.

Some valid identities are:

as it is to be false. • ∧ ≃ ∧ : ( ∧ ) • F.( ◁▷ ) ≃ : solving for = ( • ≃ ¬¬: Expanding the semantics we have (¬¬)

I = I · I = I · I = ( ∧ )

I = 1 − (1 −

I .

I + )/2 we get F.( ◁▷ ) I = I.

I) = I.

• F.( ∧ ) ◁▷ ( → ) ≃ 1/2: as discussed in Section 3, this expression is as likely to be true The first is familiar as double negation, and the second is the commutativity of conjunction. Both are typical of Boolean reasoning. The third one is a combined property of the ◁▷ operation and the fixed point. If we repeatedly sample a fair coin, it will eventually land heads.

 4.2. Theories

interpretation where every identity in Θ holds.

Having established a notion of true logical statements via identities, we can consider more than just the set of valid identities; we can consider systems that conform to a set of given identities.

Given a set of identities, Θ ⊆ Ξ , we may ask whether it is necessary that some identity holds in any Definition 6. We refer to a set of identities as a theory, and given a theory Θ and some interpretation I, such that every identity in Θ is satisfied by I, we say I satisfies Θ, written I |= Θ.

The notion of satisfiability and validity may be extended to theories.

Definition 7. If there is some interpretation I where I |= Θ we say Θ is satisfiable and if every interpretation satisfies Θ we say Θ is valid. For every identity, ≃ , if every interpretation I that satisfies Θ also satisfies ≃ , we say Θ validates ≃ , written Θ |= ≃ .

Theories impose constraints on the probabilities that atoms can represent. For example ≃ ∧ requires that I() = I()2, which only has the solutions 0 and 1, so this identities requires to be certain (always Yes or always No).

 4.3. Deductive systems

We would like to be able to describe a system of natural deduction for aleatoric identities, so that given a theory of known aleatoric identities, we are able to infer all consequential identities. To do this we require the notion of a substitution.

Definition 8. Given , ∈ ℒ and ∈ the substitution of for in (written [∖]) defined recursively as follows: [∖] = (where ̸= ), [∖] = , (¬)[∖] = ¬([∖]) 1 ∧ 2[∖] = 1[∖] ∧ 2[∖] , 1 ◁▷ 2[∖] = 1[∖] ◁▷ 2[∖] , (F )[∖] = F [∖], where ̸= , and does not occur free in , and (F)[∖] = F.

Substitutions can be applied sequentially, so given = (0, . . . , −1 ) ∈ and = ( 0, . . . , −1 ) ∈ ℒ, we write [ ∖] as an abbreviation for [ 0∖ 0] . . . [−1 ∖ −1 ].

If a substitution is defined we say it is a valid substitution. is ,

Note that the substitutions account for the free variables, so fixed point operators in will not afect the interpretation of in the substitution [∖]. The deductive system consists of inference rules. Definition 9. An aleatoric rule 1 ≃ 1, . . . , ≃ ⊢ ≃ is a pair consisting of a finite set of identities, { 1 ≃ 1, . . . , ≃ } ⊂ Ξ (the antecedent); and a single identity ≃ (the consequent). When the antecedent is the empty set we write ⊢ ≃ and refer to it as an aleatoric axiom. We refer to a set of aleatoric rules as a deductive system.

Entailment follows from the repeated application of rules, closed under substitution: Definition 10. Given a deductive system, Δ, and a theory, Θ, the Δ-closure of Θ is ΘΔ, the smallest theory where: Θ ⊆ Θ Δ; and for any rule 1 ≃ 1, . . . , ≃ ⊢ ≃ , such that 1 ≃ 1, . . . , ≃ ∈ ΘΔ we have ≃ ∈ Θ Δ.

Given some deductive system Δ and a theory, Θ, we say Θ entails ≃ in Δ if ≃ ∈ Θ Δ With these definitions we can now define the logical concepts: consistent, sound and complete. Definition 11. A theory Θ is consistent for a deductive system Δ, if ⊤ ≃ ⊥ ∈/ Θ Δ.

A deductive system Δ is consistent if ∅ is consistent for Δ.

Definition 12. A deductive system Δ is sound if for every theory Θ, and every identity ≃ ∈ Θ we have for every interpretation I that satisfies Θ, I = I. Definition 13. A deductive system Δ is complete for a theory Θ, if for every identity ≃ where Θ |= ≃ , we have ≃ ∈ Δ. A deductive system Δ: is complete if it is complete for every finite theory; is strongly complete if it is complete for every theory; and is complete for validity if it is complete for the empty theory.

Note, in many proof systems being “complete” and “complete for validity” are synonymous, since implication and conjunction allow entailment from a finite theory to be represented in a single proposition (at least for compact logics). However, implication and conjunction over identities are not available in this setting, so “complete” and “complete for validity” are quite diferent concepts.

We are now able to formulate the following questions: 1. Can we define a sound deductive system that is complete for validity? 2. Can we give a sound a complete deductive system for all theories? The diference between these two questions is non-trivial. A sound deductive system that is complete for validity only needs to generate identities that are necessarily true, for example ∧ ≃ ∧ . However, there is no concept of a negative identity, or inequality, so there is no requirement to generate ⊤ ̸≃ ⊥ for example.

This becomes important when we consider complete deductive systems for all theories. For example, the identity ∨ ¬ ≃ ∧ ¬ is not satisfiable in any interpretation 3, so { ∨ ¬ ≃ ∧ ¬} would entail ⊤ ≃ ⊥ in a complete deductive system.

 4.4. A characterisation of valid identities

In this section we present a substitution schema of axioms and rules to characterise the valid identities of aleatoric logic.

Definition 14. The deductive system, aleatory logic, (AL) consists of the following rules, where , , , are any aleatoric propositions such that rules are well formed.

id ⊢ ≃ ∧-comm ⊢ ∧ ≃ ∧ ∧-assoc ⊢ ( ∧ ) ∧ ≃ ∧ ( ∧ ) dn ⊢ ¬¬ ≃ dist-¬ ⊢ ¬( ◁▷ ) ≃ (¬) ◁▷ (¬) dist-∧ ⊢ ( ◁▷ ) ∧ ≃ ( ∧ ) ◁▷ ( ∧ ) swap ⊢ ( ◁▷ ) ◁▷ ( ◁▷ ) ≃ ( ◁▷ ) ◁▷ ( ◁▷ ) same ⊢ ◁▷ ≃ simp ⊢ ( ∧ ) ◁▷ ¬(¬ ∧ ¬) ≃ ◁▷ half ⊢ ¬F. ≃ F. amp ⊢ ¬( ∧ ) ∧ F. ≃ ¬ ◁▷ ( ∧ ¬) fp-elim ⊢ F. ≃ [∖F.] subst ≃ ⊢ [∖] ≃ [∖] trans ≃ , ≃ ⊢ ≃ fp-intro ≃ [∖] ⊢ ≃ F.(), where ̸≃ order ◁▷ ≃ ◁▷ ⊢ ≃ .

The condition on fp-intro The condition on fp-intro is in some sense circular and deserves discussion. It requires that is not identical to , as in such a case we would have (through the id axiom) that for every proposition , ≃ [∖] and so for every proposition , ⊢ ≃ F. and the whole system would collapse to a trivial singleton. Due to the linearity constraint, the only way this collapse might occur is if is identical to . It is not enough to say that is not equal to , because could take trivially equivalent forms like ◁▷ .

There are several possible ways to enforce this: syntactically we could require that has the form 1 ◁▷ 2 where does not occur in 2. This would sufice, but it is not clear that it would be general enough and it certainly complicates some otherwise simple proofs. We have included the condition for 3Substituting into Definition 3, this would require us to find a solution for 1 − 2 + 2 2 = 0 with ∈ [ 0, 1 ], which does not have any real solutions. now, as it is the simplest compromise, and may be treated as an oracle. However, more work needs to be done to ensure that it is sound and well defined. The concern is that some identity ⊢ ≃ might be inferred through an application of fp-elim assuming ̸≃ , but only from the identity ⊢ ≃ , we are able to infer ≃ . A careful argument needs to be given to justify that such a situation cannot arise.

We provide some example derivations to demonstrate the deductive system AL and establish some useful theorems.

1. F. ≃ ¬F.¬[∖¬]. That is the fixed point operator is self dual.

F. ≃ [∖F.]

F. ≃ ¬¬[∖¬][∖¬F.] ¬F. ≃ ¬[∖¬][∖¬F.] ¬F. ≃ F.¬[∖¬] ¬F. ≃ F.¬[∖¬]

F. ≃ ¬F.¬[∖¬] fp-elim

dn id, subs, dn fp-intro, if ̸≃ half, if ≃ dn 2. ≃ F.(( ∧ ) ◁▷ ( ∨ )). This equivalence is akin to a Bernoulli race: where given a test two outcomes (say heads and tails) we run the test to see if a randomly chosen outcome (heads or tails, chosen fairly) occurs, and if it does not occur, we repeat the process. The outcome of the process is identical to the original test. The proof is below: 3. ◁▷ ¬ ≃ F.. A fair choice between a test or its negation a the same as a fair coin flip. ≃ ◁▷ same ≃ ( ∧ ) ◁▷ ( ∨ ) simp ≃ (( ∧ ) ◁▷ ( ∨ ))[∖] rewriting ≃ F.(( ∧ ) ◁▷ ( ∨ ) fp-intro ( ◁▷ ¬) ≃ ( ◁▷ ¬) ≃ ( ◁▷ ¬) ≃ ( ◁▷ ¬) ≃ ( ◁▷ ¬) ≃ ( ◁▷ ¬) ≃ ( ◁▷ ¬) ≃ ¬¬( ◁▷ ¬) dn ¬(¬ ◁▷ ) dn dist-¬ ¬((¬ ◁▷ ) ◁▷ (¬ ◁▷ )) same, subs ¬(( ◁▷ ¬) ◁▷ ( ◁▷ ¬)) swap, subs ¬( ◁▷ ¬)) same, subs F.¬ fp-intro

F. (1), half

 5. Soundness

We show the soundness of the rules and axioms of AL, and provide a discussion of the axioms. Lemma 15. The deductive system AL is sound.

Proof:

We will also give some discussion of each axiom as we address them in turn. • id: ⊢ ≃ . This follows trivially since for all interpretations I, I = I. • ∧-comm: ⊢ ∧ ≃ ∧ . This follows directly from the commutativity of multiplication: for all interpretations ( ∧ ) I = I · I = I · I = ( ∧ ) I. • ∧-assoc: ⊢ ( ∧ ) ∧ ≃ ∧ ( ∧ ) . This follows from the associativity of multiplication: (( ∧ ) ∧ ) I = I · I · I = ( ∧ ( ∧ )) I. • dn: ⊢ ¬¬ ≃ . This is the standard double negation axiom: (¬¬) I = 1 − (1 − I) = I. • dist-¬: ⊢ ¬( ◁▷ ) ≃ (¬) ◁▷ (¬) . Negation distributes over the aleatoric or operator: (¬( ◁▷ )) I = 1 − ( I + I)/2 = ((1 − I) + (1 − I))/2 = ((¬) ◁▷ ¬)) I. • dist-∧: ⊢ ( ◁▷ ) ∧ ≃ ( ∧ ) ◁▷ ( ∧ ) . Conjunction also distributes over aleatoric or: (( ◁▷ ) ∧ ) I = (( I + I)/2) · I = ( I · I + I · I)/2 = (( ∧ ) ◁▷ ( ∧ )) I • swap: ⊢ ( 1 ◁▷ 2) ◁▷ ( 1 ◁▷ 2) ≃ ( 2 ◁▷ 2) ◁▷ ( 1 ◁▷ 1). This axiom captures the limited associativity and commutativity of the aleatoric or operator. As the aleatoric or operation is essentially a weighted sum (in fact an average), we can change the order of the operands, provided we preserve the depth of nesting. For all interpretations I, (( 1 ◁▷ 2) ◁▷ ( 1 ◁▷ 2))I = ( 1I + 2I + 1I + 2I)/4 = (( 2 ◁▷ 2) ◁▷ ( 1 ◁▷ 1))I. • same: ⊢ ◁▷ ≃ . As aleatoric or works as an average, it is idempotent: ( ◁▷ ) I = ( I + I)/2 = I. • simp: ⊢ ( ∧ ) ◁▷ ¬(¬ ∧ ¬) ≃ ◁▷ . This simplification rule is interesting, and not obvious.

It reflects an interesting logic puzzle, where you are given a coin with an unknown bias, and you can choose to flip it once (winning if it lands heads), or flip it twice, but if you flip it twice you will only win if it lands heads times, where is randomly chosen to be 1 or 2 (with equal chance). It can be shown that your chance of winning remains the same regardless of your choice. In terms of this axiom: (( ∧ ) ◁▷ ¬(¬ ∧ ¬))

I = (( I · I) + ( I + I − = ( I · I)/2 = ( ◁▷ ) I.

I · I))/2 • half : ⊢ F. ≃ ¬F.. As mathematically every value is a fixed point of , this axiom defines the fixed point in this case to be 1/2. Note that the semantics could have also been defined to use a greatest fixed point ( (F.)I = 1), or a least fixed point ( (F.)I = 0), and these semantics could also remove the linearity constraint on fixed point variables, so in the greatest ifxed point semantics (F.(( ∨ ) ∧ ¬) = (3 − √5)/2. Such semantic variations are left to future work. The soundness of the axiom is a direct application of the semantics. • amp: ⊢ ¬( ∧ ) ∧ F. ≃ ¬ ◁▷ ( ∧ ¬) . This is an interesting axiom, named amp for aleatoric modus ponens, as it may be rewritten as ( → ) ∧ F. ≃ ¬ ◁▷ ( ∧ ) (substituting for ¬ ). Ignoring the factor of a half on the left side (F.) this could be read as implies is the same as either ¬ or ∧ , where or is interpreted aleatorically. In this way, it gives a sense of a deductive operation similar to modus ponens. The soundness follows as: (¬( ∧ ) ∧ F.)

I = (1 − = (1 − = ((1 − = (¬ ◁▷ ( ∧ ¬))

I · I) · 1/2 I + I −

I · I)/2 I) + ( I) · (1 −

I.

I))/2 • fp-elim: ⊢ F. ≃ [∖F.] . This is the standard fixed point definition. Note that in Definition 8, [∖F.] is only defined if is free for in . That is, no free variable of can become bound in the substitution. Soundness follows since (F.) I = where I[←] = . As the semantics are recursive and (F.) I = , I[←] = [∖F.] I as required. • subst: ≃ ⊢ [∖] ≃ [∖] . As the semantics are given recursively, substituting equivalent propositions into the same form will give equivalent propositions. Note that a substitution [∖] is only defined if is free for in . Also, note that the order of and are switched so this axiom also establishes the symmetry of the ≃ relation. From ≃ , and the substitution instance of id: ≃ , the subst rule allows us to derive ≃ . • trans: ≃ , ≃ ⊢ ≃ . This rule simply establishes ≃ as a transitive relation, which follows trivially from the transitivity of equality. This rule along with the axiom id and the subst rule is enough to ensure that ≃ is an equivalence relation. • fp-intro: ≃ [∖] ⊢ ≃ F.(), where ̸≃ . This rule allows a fixed point operator to be introduced, where a fixed point has been deduced. That is, if I = [∖] I, then I is a fixed point of in . However, there is a problem in that may not be the only fixed point in (and exclusively in) the case that is identical to (see Lemma 4). As discussed above, the condition that ̸≃ is somewhat problematic, but it is the best compromise we have for now. • order: ◁▷ ≃ ◁▷ ⊢ ≃ . This rule is sound since if ( I + I)/2 = ( I + I)/2, then multiplying both sides of the equation by 2 and subtracting I is enough to show I = I. This rule is required particularly for showing completeness for theories, where equivalences may be stated without being able to be reduced to common elements. That is, we can derive such equivalences where they necessarily hold in all interpretations, but give a theory that specifies ◁▷ ≃ ◁▷ , we will have I/2 + I/2 = I/2 + I/2 so can derive I = I. We have shown all the rules of AL to be sound.

 6. Completeness for Validity

□ The completeness of the system AL is conjectured, but remains an open question. Conjecture 16. The deductive system AL is complete for the validity of aleatoric logic.

The proposed proof of completeness for validity will proceed with the following steps: 1. Introduce a normal form for aleatoric propositions, referred to as aleatoric normal form (anf). 2. Show that every aleatoric proposition is provably equivalent to a proposition in anf. 3. Show a partial correspondence between anf and the rational functions from [ 0, 1 ] to [ 0, 1 ]. 4. Show that when two propositions in anf correspond to the same rational function, then they are provably equivalent.

6.1. Aleatoric Normal Form

Aleatoric Normal Form shows that every proposition can be efectively represented by repeated Bernoulli Tests over a finite set of propositional atoms. This normal form has previously been exploited to give an expressiveness completeness result in [ 1 ].

Definition 17. Let be a reserved atom in ℒ. The set of propositions in -aleatoric normal form is generated by the following Backus-Naur form:

conj clause− anf−

= | ¬ | conj ∧ conj = | (¬conj ∧ ) | (conj ∨ ) | clause ◁▷ clause = F.clause Where is clear from context we just refer to aleatoric normal form, anf.

This normal form is closely related to the -block normal form of [ 1 ], which was applied to show that aleatoric logic was expressively complete for the set of rational functions from [ 0, 1 ] to (0, 1).

Definition 18.

als ℓ and :

A rational function, : (0, 1) →− (0, 1) is a -block-function if there exists polynomiℓ( ) = ∑︀∈ ℓ ∏︀∈ ( ) = ∑︀∈ ∏︀∈ (,+) · (1 − ) (,−) (,+) · (1 − ) (,−) where = { ∈ {0, . . . , } ×{+,−} | ∑︀∈ (,+) + (,−) integers such that ℓ < and ( ) = ℓ( )/( ). = }, for all ∈ , ℓ and are A -block function is designed to correspond to to the notion of -block normal form aleatoric propositions, and also has an elegant correspondence to rational functions : [ 0, 1 ] →− (0, 1). Lemma 19. Given some rational function : [ 0, 1 ] →− (0, 1) , there is some -block function ′ : [ 0, 1 ] →− (0, 1) such that ( ) = ′( ).

This is applied in [ 1 ] to give the following theorem.

Theorem 20. 1. For every aleatoric proposition ∈ ℒ defined over the free variables in , ( ) is a rational function from (0, 1) to (0, 1). 2. For -block-function ( ) from (0, 1) to (0, 1), there is some aleatoric proposition such that ( ) = ( ). 3. For every rational function ( ) from [ 0, 1 ] to (0, 1), there is some aleatoric proposition such that ( ) = ( ).

This motivates the proposed proof structure that we have given. While the result in [ 1 ] is a purely semantic argument, the aim here is to formalise it in the deductive system AL. The reduction to rational functions gives both a notion of equivalence (that of being functionally equivalent) and also a notion of irreducibility: an aleatoric proposition in aleatoric normal form is irreducible if the numerator and denominator of the corresponding rational function are co-prime.

The first conjecture required for the completeness proof is as follows: Conjecture 21. Every aleatoric proposition, , is equivalent to some proposition ^ in aleatoric normal form, where ≃ ^is provable in AL.

This is likely to be shown via an inductive transformation, showing each step is provably correct. One of the more dificult steps is applying a version of the distributivity property required for the clause− normal form. It can be shown that ∧ ¬( ∧ ) ≃ F ⎡ (( ∧ ¬) ∨ ) ◁▷ (( ∧ ∧ ¬) ∨ ) ⎣ ◁▷ ( ∧ ) ◁▷ (¬( ∧ ∧ ) ∧ ) ⎤ ⎦ Given is in aleatoric normal form, it can be written as where and are of the form or ¬ where ∈ . Here, the aleatoric-or operation (◁▷) is applied uniformly to a set of propositions, so for example, F ◁▷ [ 1, 2, 3] is an abbreviation for F.(( 1 ◁▷ 2) ◁▷ ( 3 ◁▷ )). This representation is reminiscent of a truth table representation used in Boolean propositional logic: the rows are the combinations of variables that are specified as true; and the rows are the combinations of variables that are specified as false. However, the nature of aleatoric logic replaces the “combinations of variables” with multi-sets of positive and negative atoms.

Letting be an arithmetical variable, and ¬ be (1− ), we can show that the semantic interpretation of is equivalent to the multivariate rational function: =

∑︀=1 ∏︀=1 ∑︀=1 ∏︀=1 + ∑︀ =1 ∏︀ =1 Now it is possible that the numerator and denominator of this rational function have a common factor. The following conjecture is required: Conjecture 22. Every aleatoric proposition, , is equivalent to some proposition * in aleatoric normal form, where ≃ * is provable in AL, and * is an irreducible rational function, in the sense that the numerator and the denominator are relatively prime.

The completeness then follows from the following conjecture: Conjecture 23. Given two propositions, and , where: 1. and are in aleatoric normal form; 2. and are equivalent, irreducible rational functions; 3. and are equivalent rational function; we can show ≃ in AL.

This conjecture follows from the swap, ∧-comm and ∧-assoc axioms.

These conjectures are suficient to give the completeness of AL: by Conjecture 22, any two semantically equivalent propositions, and , must have irreducible aleatoric normal form variants * and * where ≃ * , ≃ * such that * and * are functionally equivalent. By Conjecture 23, we have * ≃ * , and the result follows by the trans rule.

 Declaration on Generative AI

The author(s) have not employed any Generative AI tools.

 [1] T. French , Aleatoric propositions: Reasoning about coins , in: Logic, Language, Information, and Computation: 2023, Proceedings, 2023 , pp. 227 - 243 . [2] T. French , A. Gozzard , M. Reynolds , A modal aleatoric calculus for probabilistic reasoning , in: Logic and Its Applications: ICLA 2019 , 2019 , pp. 52 - 63 . [3] A. N. Kolmogorov , The theory of probability, Mathematics, Its Content, Methods, and Meaning 2 ( 1963 ) 110 - 118 . [4] F. P. Ramsey , The foundations of mathematics , Oxford University Press, 1925 . [5] B. De Finetti , Theory of probability: a critical introductory treatment , John Wiley & Sons, 1970 . [6] J. Halpern , Reasoning about Uncertainty , MIT Press, Cambridge MA, 2003 . [7] D. Kozen , A probabilistic PDL , Journal of Computer and System Sciences 30 ( 1985 ) 162 - 178 . [8] P. Gärdenfors , Qualitative probability as an intensional logic , Journal of Philosophical Logic ( 1975 ) 171 - 185 . [9] Y. Pan , M. Guo , Probabilistic epistemic logic based on neighborhood semantics , Synthese 203 ( 2024 ) 135 . [10] L. A. Zadeh , Fuzzy sets , in: Fuzzy Sets, Fuzzy Logic , And Fuzzy Systems: Selected Papers by Lotfi A Zadeh , World Scientific, 1996 , pp. 394 - 432 . [11] P. Hajek , Metamathematics of Fuzzy Logic, Kluwer Academic Press, 1998 . [12] A. Madeira , R. Neves , M. A. Martins , An exercise on the generation of many-valued dynamic logics , Journal of Logical and Algebraic Methods in Programming 85 ( 2016 ) 1011 - 1037 . [13] O. Majer , I. Sedlár , On many-valued modal probabilistic logics , in: 2025 IEEE 55th International Symposium on Multiple-Valued Logic (ISMVL) , IEEE Computer Society , 2025 , pp. 26 - 31 . [14] J. Pavelka , On fuzzy logic i many-valued rules of inference , Mathematical Logic Quarterly 25 ( 1979 ) 45 - 52 . [15] F. Esteva , L. Godo, Monoidal t-norm based logic:towards a logic for left-continuous t-norms , Fuzzy Sets and Systems 124 ( 2001 ) 271 - 288 . Fuzzy Logic.