B Is this equation at all sensical?

Click For Summary
The discussion revolves around the interpretation of a logical expression involving time and conditions, specifically ∀t(T(x,t)⟹(¬H(x,t)∨H(x,t+Δt))). Participants note the lack of context makes it challenging to derive meaning, with some suggesting it may relate to formal hardware description languages or theorem proving systems like ACL2. The expression implies relationships between variables over time, indicating transitions in truth values. There is also mention of its potential connection to logical operators and the Boyer-Moore Theorem Prover. Overall, the conversation highlights the complexities of interpreting abstract logical statements without sufficient context.
DaveC426913
Gold Member
Messages
23,991
Reaction score
8,128
TL;DR
This looks like nonsense, or at least nothing meaningful.
(Yes, I'm guilty of passing along something incomplete and of utterly unknown provenance that someone saw somewhere and didn't understand. I feel dirty.)


∀t(T(x,t)⟹(¬H(x,t)∨H(x,t+Δt)))

Certainly, without specifying any of the variables, it's got to be useless. At least we can assume t and Δt refer to time/delta time - which is my rationale for posting here in the physics subforum)

Chat GPT made a broad guess but couldn't make heads or tails of it either. Don't judge me.
 
Physics news on Phys.org
I would normally interpret those symbols as logical operators, so you might be better asking in the relevant maths forum. Difficult to tell without context, though.
 
∀t(T(x,t)⟹(¬H(x,t)∨H(x,t+Δt)))
For all t, T(x,t) implies ( NOT( H(x,t) ) OR H(x,t+Δt) )
T(x,t) is FALSE if H(x,t) was TRUE, and H(x,t+Δt) is FALSE.
T(x,t) is FALSE when H(x,t) transitions to FALSE in next sample.
A negative edge in H causes T to go low for one cycle.

Maybe it is from a formal HDL used to describe logic functions.
 
  • Like
Likes SammyS, Ibix and PeroK
It looks a bit like input code for a Boyer-Moore Theorem Prover.
Example here: https://en.wikipedia.org/wiki/Nqthm#Theorem_formulation
"(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))"

ACL2 or "A Computational Logic for Applicative Common Lisp", an applicative (side-effect free) variant of Common LISP. ACL2 is both a programming language which can model computer systems, and a tool to help proving properties of those models.
 
Thread 'The rocket equation, one more time'
I already posted a similar thread a while ago, but this time I want to focus exclusively on one single point that is still not clear to me. I just came across this problem again in Modern Classical Mechanics by Helliwell and Sahakian. Their setup is exactly identical to the one that Taylor uses in Classical Mechanics: a rocket has mass m and velocity v at time t. At time ##t+\Delta t## it has (according to the textbooks) velocity ##v + \Delta v## and mass ##m+\Delta m##. Why not ##m -...

Similar threads

  • · Replies 4 ·
Replies
4
Views
4K
  • · Replies 13 ·
Replies
13
Views
21K
Replies
2
Views
4K
  • · Replies 7 ·
Replies
7
Views
2K
  • · Replies 10 ·
Replies
10
Views
1K
  • · Replies 4 ·
Replies
4
Views
2K
  • · Replies 5 ·
Replies
5
Views
1K
  • · Replies 7 ·
Replies
7
Views
1K
Replies
1
Views
1K
  • · Replies 4 ·
Replies
4
Views
2K