Propositional functions are propositional formulas up to semantic equivalence.
@JamesGallicchio I thought about your question of whether we want to use this or { f: PropAssignment ν → Bool | dependsOnFinitelyManyVars f } as the mathematical model, in particular in cases where we have a function but don't want to construct a prop. formula. I think the two definitions should be equivalent, but the current one is easier to make because it doesn't require defining dependsOnFinitelyManyVars first (I will add that in a later PR). We can deal with the non-formula issue later by proving that any function depending on a finite amount of vars can be encoded as a formula, essentially by picking an ordering on the variables it depends on and then doing iterated Shannon expansions (or constructing a non-reduced OBDD, if you want).
Vtec234
commented
1 year ago
Propositional functions are propositional formulas up to semantic equivalence.
@JamesGallicchio I thought about your question of whether we want to use this or
{ f: PropAssignment ν → Bool | dependsOnFinitelyManyVars f }as the mathematical model, in particular in cases where we have a function but don't want to construct a prop. formula. I think the two definitions should be equivalent, but the current one is easier to make because it doesn't require definingdependsOnFinitelyManyVarsfirst (I will add that in a later PR). We can deal with the non-formula issue later by proving that any function depending on a finite amount of vars can be encoded as a formula, essentially by picking an ordering on the variables it depends on and then doing iterated Shannon expansions (or constructing a non-reduced OBDD, if you want).