High School 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
24,077
Reaction score
8,211
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.
 
Topic about reference frames, center of rotation, postion of origin etc Comoving ref. frame is frame that is attached to moving object, does that mean, in that frame translation and rotation of object is zero, because origin and axes(x,y,z) are fixed to object? Is it same if you place origin of frame at object center of mass or at object tail? What type of comoving frame exist? What is lab frame? If we talk about center of rotation do we always need to specified from what frame we observe?

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
2K
  • · Replies 4 ·
Replies
4
Views
2K