Created at: Wednesday, 18 June 2025 2:15:55 am Last Modify: Wednesday, 18 June 2025 2:15:55 am

Formal Logic

Syntax

abstract sig Address {}
sig AttackerAddress extends Address {}

one sig SDPOffer, SDPAnswer, SDPCandidates, Connect 
  extends MessageType {}

pred XXXX {

}
fact{}
assert XXXX{}
check XXXX{

}

Logics

Propositions

A statement in logic that is either true or false

Connectives

Name	Notation
and	∧
or	∨
not	¬
implies	⇒ (or →)
iff	⇔

Variables

Variables allow propositions to talk about state

Sets

A collection of things

{3,5}

{ x | even[x] }

Set Operations

Operation	Notation
Union	A+B
Intersection	A&B
Difference	A-B
Disjoint	no A&B
Subset	A in B

Predicates

Extend propositions with the ability to quantify the values of a variable that a proposition is true for

all: Proposition P(x) holds for all values of x

all x | P[x]

some: Proposition P(x) holds for at least one value of x

some x | P[x]

Quantification

De Morgan’s Laws

all x | P[x] is equivalent to not some x | not P[x]

some x | P[x] is equivalent to not all x | not P[x]

Alloy specific

notion	meaning
one x	P[x]|P(x) holds for exactly one value x
lone x	P[x]|P(x) holds for at most one value x
none x	P[x]|P(x) holds for no value x

Relations

A proposition that relates things togethe

arity: the number of things the relation relates

=, < etc. are all binary relations; relate two numbers

A relation that relates three things together:

IsSum(x,y,z) ⇔ z = x + y

Relations are just predicates

What is relation

Simplest answer: just list all of the things it relates together.

Any relation is a simply a set of tuples.

Relations as Sets

A binary (2-ary) relation R(a,b) is a set of: pairs

A ternary (3-ary) relation R(a,b,c) is a set of: triples

A unary (1-ary) relation R(a) is a set of: atoms

Sets are relations, and relations are sets.

Sets are predicates, and predicates are sets.

Relations are predicates, and predicates are relations.